Theorems · Theorem · order theory

GroupCone.mk.injEq

∀ {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

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

CommGroup