Theorems · Definition · group theory
Submonoid.fromLeftInv
{M : Type u_1} → [inst : Monoid M] → (S : Submonoid M) → ↥S.leftInv → ↥SThe function from S.leftInv to S sending an element to its right inverse in S.
This is a MonoidHom when M is commutative.
- Defined in
- Mathlib.GroupTheory.Submonoid.Inverses
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- Submonoidstatement and proof · cited by 3,086
- Submonoid.leftInvstatement and proof · cited by 20
Cited by9
Results whose statement or proof uses this declaration.
- Submonoid.mul_fromLeftInvstatement · cited by 5
- Submonoid.fromCommLeftInvproof · cited by 2
- Submonoid.fromLeftInv_mulstatement and proof · cited by 1
- Submonoid.fromCommLeftInv_applystatement · cited by 0
- Submonoid.fromLeftInv_eq_iffstatement · cited by 0
- Submonoid.fromLeftInv_eq_invstatement and proof · cited by 0
- Submonoid.fromLeftInv_leftInvEquiv_symmstatement · cited by 0
- Submonoid.fromLeftInv_onestatement and proof · cited by 0
- Submonoid.leftInvEquiv_symm_fromLeftInvstatement · cited by 0