Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-11 21:21 cc5ff8ca

View on Github →

feat(group_theory/submonoid): The submonoid of left inverses of a submonoid (#10679)

Estimated changes

Modified src/algebra/group/units.lean

Modified src/group_theory/submonoid/basic.lean

Created src/group_theory/submonoid/inverses.lean

added def submonoid.from_comm_left_inv

added def submonoid.from_left_inv

added theorem submonoid.from_left_inv_eq_iff

added theorem submonoid.from_left_inv_eq_inv

added theorem submonoid.from_left_inv_left_inv_equiv_symm

added theorem submonoid.from_left_inv_mul

added theorem submonoid.from_left_inv_one

added theorem submonoid.is_unit.submonoid.coe_inv

added def submonoid.left_inv

added theorem submonoid.left_inv_eq_inv

added def submonoid.left_inv_equiv

added theorem submonoid.left_inv_equiv_mul

added theorem submonoid.left_inv_equiv_symm_eq_inv

added theorem submonoid.left_inv_equiv_symm_from_left_inv

added theorem submonoid.left_inv_equiv_symm_mul

added theorem submonoid.left_inv_le_is_unit

added theorem submonoid.left_inv_left_inv_eq

added theorem submonoid.left_inv_left_inv_le

added theorem submonoid.mul_from_left_inv

added theorem submonoid.mul_left_inv_equiv

added theorem submonoid.mul_left_inv_equiv_symm

added theorem submonoid.unit_mem_left_inv