Theorems · Theorem · order theory

GroupCone.mk.inj

∀ {G : Type u_1} {inst : CommGroup G} {toSubmonoid : Submonoid G}
  {eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1}
  {toSubmonoid_1 : Submonoid G}
  {eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1},
  { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem' } =
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'_1 } →
    toSubmonoid = toSubmonoid_1

Defined in

Mathlib.Algebra.Order.Group.Cone

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext