Theorems · Definition · order theory

GroupCone.recOn

{G : Type u_1} →
  [inst : CommGroup G] →
    {motive : GroupCone G → Sort u} →
      (t : GroupCone G) →
        ((toSubmonoid : Submonoid G) →
            (eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1) →
              motive { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem' }) →
          motive t

Defined in: Mathlib.Algebra.Order.Group.Cone
Cited by: 0 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext
Assumes: CommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Submonoidstatement and proof · cited by 3,086
CommGroupstatement and proof · cited by 990
Subsemigroup.carrierstatement and proof · cited by 160
Submonoid.toSubsemigroupstatement and proof · cited by 159
GroupConestatement and proof · cited by 7

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.