Commit 2023-02-02 13:45 774069a7

View on Github →

feat: port GroupTheory.Submonoid.Inverses (#1987)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Submonoid/Inverses.lean

added theorem Submonoid.IsUnit.Submonoid.coe_inv

added theorem Submonoid.fromLeftInv_eq_iff

added theorem Submonoid.fromLeftInv_eq_inv

added theorem Submonoid.fromLeftInv_leftInvEquiv_symm

added theorem Submonoid.fromLeftInv_mul

added theorem Submonoid.fromLeftInv_one

added def Submonoid.leftInv

added theorem Submonoid.leftInvEquiv_mul

added theorem Submonoid.leftInvEquiv_symm_eq_inv

added theorem Submonoid.leftInvEquiv_symm_fromLeftInv

added theorem Submonoid.leftInvEquiv_symm_mul

added theorem Submonoid.leftInv_eq_inv

added theorem Submonoid.leftInv_le_is_unit

added theorem Submonoid.leftInv_leftInv_eq

added theorem Submonoid.leftInv_leftInv_le

added theorem Submonoid.mul_fromLeftInv

added theorem Submonoid.mul_leftInvEquiv

added theorem Submonoid.mul_leftInvEquiv_symm

added theorem Submonoid.unit_mem_leftInv