Theorem ofDual_eq_one

Modification history

2025-12-20 10:21
Mathlib/Algebra/Order/Group/Synonym.lean
chore(Algebra): fix whitespace (#32906)
Modified ofDual_eq_oneView on Github →
2025-11-18 16:33
Mathlib/Algebra/Order/Group/Synonym.lean
feat: characterise regular elements of type synonyms (#31739)
Added ofDual_eq_oneView on Github →