Theorems · Definition · group theory
AddSubmonoid.fromLeftNeg
{M : Type u_1} → [inst : AddMonoid M] → (S : AddSubmonoid M) → ↥S.leftNeg → ↥SThe function from S.leftAdd to S sending an element to its right additive
inverse in S. This is an AddMonoidHom 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
- AddMonoid
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.
- AddMonoidstatement and proof · cited by 2,864
- AddSubmonoidstatement and proof · cited by 1,178
- AddSubmonoid.leftNegstatement and proof · cited by 19
Cited by9
Results whose statement or proof uses this declaration.
- AddSubmonoid.add_fromLeftNegstatement · cited by 5
- AddSubmonoid.fromCommLeftNegproof · cited by 2
- AddSubmonoid.fromLeftNeg_addstatement and proof · cited by 1
- AddSubmonoid.leftNegEquiv_symm_fromLeftNegstatement · cited by 0
- AddSubmonoid.fromCommLeftNeg_applystatement · cited by 0
- AddSubmonoid.fromLeftNeg_eq_iffstatement · cited by 0
- AddSubmonoid.fromLeftNeg_eq_negstatement and proof · cited by 0
- AddSubmonoid.fromLeftNeg_leftNegEquiv_symmstatement · cited by 0
- AddSubmonoid.fromLeftNeg_zerostatement and proof · cited by 0