Theorems · Definition · order theory

GroupCone.mk.noConfusion

{G : Type u_1} →
  {inst : CommGroup G} →
    {P : Sort u} →
      {toSubmonoid : Submonoid G} →
        {eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1} →
          {toSubmonoid' : Submonoid G} →
            {eq_one_of_mem_of_inv_mem'' : ∀ {a : G}, a ∈ toSubmonoid'.carrier → a⁻¹ ∈ toSubmonoid'.carrier → a = 1} →
              { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem' } =
                  { toSubmonoid := toSubmonoid', eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'' } →
                (toSubmonoid ≍ toSubmonoid' → P) → P

Defined in

Mathlib.Algebra.Order.Group.Cone

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext