Skip to content

[Merged by Bors] - feat(RingTheory/Nilpotents): basic MulOpposite lemmas for IsNilpotent/IsReduced #42625

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
vlad902 wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(RingTheory/Nilpotents): basic MulOpposite lemmas for IsNilpotent/IsReduced #42625

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
fdab98d
feat(RingTheory/Nilpotents): basic MulOpposite lemmas for `IsNilpoten…
vlad902 Aug 10, 2026
c4616ae
-simp lemma
vlad902 Aug 10, 2026
8597301
Update Mathlib/RingTheory/Nilpotent/Defs.lean
vlad902 Aug 11, 2026
81092a0
Update Mathlib/RingTheory/Nilpotent/Defs.lean
vlad902 Aug 11, 2026
beeca9c
Merge branch 'master' into nilpotent-reduced-mulopposite
vlad902 Aug 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions Mathlib/RingTheory/Nilpotent/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,20 @@ 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 := by
simp_rw [IsNilpotent, ← MulOpposite.op_pow, MulOpposite.op_eq_zero_iff]

alias ⟨_, IsNilpotent.op⟩ := isNilpotent_op

@[simp]
theorem isNilpotent_unop [MonoidWithZero R] {x : Rᵐᵒᵖ} :
IsNilpotent (MulOpposite.unop x) ↔ IsNilpotent x :=
isNilpotent_op.symm

alias ⟨_, IsNilpotent.unop⟩ := isNilpotent_unop

section NilpotencyClass

section ZeroPow
Expand Down Expand Up @@ -120,6 +134,13 @@ end MonoidWithZero

end NilpotencyClass

@[simp]
theorem isReduced_mulOpposite_iff [MonoidWithZero R] : IsReduced Rᵐᵒᵖ ↔ IsReduced R := by
simp [isReduced_iff]

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] :
Expand Down
Loading