Theorem Submonoid.IsUnit.Submonoid.coe_inv

Modification history

2026-05-25 15:44
Mathlib/GroupTheory/Submonoid/Inverses.lean
fix: decls with a non-consecutive duplicate namespace (#39794) …
Deleted Submonoid.IsUnit.Submonoid.coe_invView on Github →
2023-02-02 13:45
Mathlib/GroupTheory/Submonoid/Inverses.lean
feat: port GroupTheory.Submonoid.Inverses (#1987)
Added Submonoid.IsUnit.Submonoid.coe_invView on Github →