From fdab98d20b88766dbcd8d4aeb2de1a489ae93651 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Mon, 10 Aug 2026 23:42:55 +0200 Subject: [PATCH 1/4] feat(RingTheory/Nilpotents): basic MulOpposite lemmas for `IsNilpotent`/`IsReduced` --- Mathlib/RingTheory/Nilpotent/Defs.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Mathlib/RingTheory/Nilpotent/Defs.lean b/Mathlib/RingTheory/Nilpotent/Defs.lean index 4108190b2a5f23..88d44365c8344d 100644 --- a/Mathlib/RingTheory/Nilpotent/Defs.lean +++ b/Mathlib/RingTheory/Nilpotent/Defs.lean @@ -52,6 +52,22 @@ theorem IsUnit.isNilpotent_unit_mul_of_commute_iff [MonoidWithZero R] {r u : R} IsNilpotent (u * r) ↔ IsNilpotent r := h_comm ▸ hu.isNilpotent_mul_unit_of_commute_iff h_comm +@[simp] +theorem isNilpotent_op [MonoidWithZero R] {x : R} : + IsNilpotent (MulOpposite.op x) ↔ IsNilpotent x := + ⟨fun ⟨n, hn⟩ ↦ ⟨n, MulOpposite.op_injective (by simpa)⟩, + fun ⟨n, hn⟩ ↦ ⟨n, by simpa [← MulOpposite.op_pow]⟩⟩ + +alias ⟨_, IsNilpotent.op⟩ := isNilpotent_op + +@[simp] +theorem isNilpotent_unop [MonoidWithZero R] {x : Rᵐᵒᵖ} : + IsNilpotent (MulOpposite.unop x) ↔ IsNilpotent x := + ⟨fun ⟨n, hn⟩ ↦ ⟨n, by simpa [← MulOpposite.unop_eq_zero_iff]⟩, + fun ⟨n, hn⟩ ↦ ⟨n, MulOpposite.op_injective (by simpa)⟩⟩ + +alias ⟨_, IsNilpotent.unop⟩ := isNilpotent_unop + section NilpotencyClass section ZeroPow @@ -120,6 +136,13 @@ end MonoidWithZero end NilpotencyClass +@[simp] +theorem isReduced_mulOpposite_iff [MonoidWithZero R] : IsReduced Rᵐᵒᵖ ↔ IsReduced R := by + simp [isReduced_iff, isNilpotent_op] + +instance [MonoidWithZero R] [IsReduced R] : IsReduced Rᵐᵒᵖ := + isReduced_mulOpposite_iff.mpr ‹_› + theorem isReduced_of_injective [MonoidWithZero R] [MonoidWithZero S] {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S] (f : F) (hf : Function.Injective f) [IsReduced S] : From c4616ae0b45f114558da4bbd5b68ec405e1332ee Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Mon, 10 Aug 2026 23:59:04 +0200 Subject: [PATCH 2/4] -simp lemma --- Mathlib/RingTheory/Nilpotent/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Nilpotent/Defs.lean b/Mathlib/RingTheory/Nilpotent/Defs.lean index 88d44365c8344d..21de1260a4b092 100644 --- a/Mathlib/RingTheory/Nilpotent/Defs.lean +++ b/Mathlib/RingTheory/Nilpotent/Defs.lean @@ -138,7 +138,7 @@ end NilpotencyClass @[simp] theorem isReduced_mulOpposite_iff [MonoidWithZero R] : IsReduced Rᵐᵒᵖ ↔ IsReduced R := by - simp [isReduced_iff, isNilpotent_op] + simp [isReduced_iff] instance [MonoidWithZero R] [IsReduced R] : IsReduced Rᵐᵒᵖ := isReduced_mulOpposite_iff.mpr ‹_› From 859730152f870785279f37ae9d87fda899e4ef76 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Tue, 11 Aug 2026 08:10:27 +0200 Subject: [PATCH 3/4] Update Mathlib/RingTheory/Nilpotent/Defs.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/Nilpotent/Defs.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Nilpotent/Defs.lean b/Mathlib/RingTheory/Nilpotent/Defs.lean index 21de1260a4b092..01392a09d42d68 100644 --- a/Mathlib/RingTheory/Nilpotent/Defs.lean +++ b/Mathlib/RingTheory/Nilpotent/Defs.lean @@ -54,9 +54,8 @@ theorem IsUnit.isNilpotent_unit_mul_of_commute_iff [MonoidWithZero R] {r u : R} @[simp] theorem isNilpotent_op [MonoidWithZero R] {x : R} : - IsNilpotent (MulOpposite.op x) ↔ IsNilpotent x := - ⟨fun ⟨n, hn⟩ ↦ ⟨n, MulOpposite.op_injective (by simpa)⟩, - fun ⟨n, hn⟩ ↦ ⟨n, by simpa [← MulOpposite.op_pow]⟩⟩ + IsNilpotent (MulOpposite.op x) ↔ IsNilpotent x := by + simp_rw [IsNilpotent, ← MulOpposite.op_pow, MulOpposite.op_eq_zero_iff] alias ⟨_, IsNilpotent.op⟩ := isNilpotent_op From 81092a0a89a9dc9711eaa6816f98d9580dff353c Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Tue, 11 Aug 2026 08:10:36 +0200 Subject: [PATCH 4/4] Update Mathlib/RingTheory/Nilpotent/Defs.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/Nilpotent/Defs.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Nilpotent/Defs.lean b/Mathlib/RingTheory/Nilpotent/Defs.lean index 01392a09d42d68..c794aaf6892988 100644 --- a/Mathlib/RingTheory/Nilpotent/Defs.lean +++ b/Mathlib/RingTheory/Nilpotent/Defs.lean @@ -62,8 +62,7 @@ alias ⟨_, IsNilpotent.op⟩ := isNilpotent_op @[simp] theorem isNilpotent_unop [MonoidWithZero R] {x : Rᵐᵒᵖ} : IsNilpotent (MulOpposite.unop x) ↔ IsNilpotent x := - ⟨fun ⟨n, hn⟩ ↦ ⟨n, by simpa [← MulOpposite.unop_eq_zero_iff]⟩, - fun ⟨n, hn⟩ ↦ ⟨n, MulOpposite.op_injective (by simpa)⟩⟩ + isNilpotent_op.symm alias ⟨_, IsNilpotent.unop⟩ := isNilpotent_unop