Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.unit_mem_left_inv

Modification history

2022-01-05 23:45
src/group_theory/submonoid/inverses.lean
chore(*): notation for `units` (#11236)
Modified submonoid.unit_mem_left_invView on Github →
2021-12-11 21:21
src/group_theory/submonoid/inverses.lean
feat(group_theory/submonoid): The submonoid of left inverses of a submonoid (#10679)
Added submonoid.unit_mem_left_invView on Github →