Mathlib v3 is deprecated. Go to Mathlib v4

Def submonoid.from_comm_left_inv

Modification history

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.from_comm_left_invView on Github →