Theorems · Theorem · group theory

AddSubmonoid.leftNegEquiv_apply

∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (a : ↥S.leftNeg),
  (S.leftNegEquiv hS) a = (↑S.fromCommLeftNeg).toFun a

Defined in

Mathlib.GroupTheory.Submonoid.Inverses

Cited by

2 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid