Theorem eq_of_mul_eq_add_eq_one

Modification history

2025-04-13 02:25
Mathlib/Algebra/Order/Ring/Idempotent.lean
chore(*): rename ring type variables (#23939) …
Modified eq_of_mul_eq_add_eq_oneView on Github →
2025-04-10 13:15
Mathlib/Algebra/Order/Ring/Idempotent.lean
feat: generalize Mathlib.Algebra.Order + Polynomial (#23153) …
Modified eq_of_mul_eq_add_eq_oneView on Github →
2025-01-10 20:46
Mathlib/Order/Idempotents.lean
feat(Order): Boolean algebra structure on idempotents (#20618) …
Added eq_of_mul_eq_add_eq_oneView on Github →