Theorems · Definition · number theory

IsHeckeTriple.recOn

{G : Type u_1} →
  [inst : Group G] →
    {Δ : Submonoid G} →
      {H₁ H₂ : Subgroup G} →
        {motive : IsHeckeTriple Δ H₁ H₂ → Sort u} →
          (t : IsHeckeTriple Δ H₁ H₂) →
            ((left_le : H₁.toSubmonoid ≤ Δ) →
                (right_le : H₂.toSubmonoid ≤ Δ) →
                  (commensurable : H₁.Commensurable H₂) →
                    (le_commensurator_right : Δ ≤ (Subgroup.Commensurable.commensurator H₂).toSubmonoid) → motive ⋯) →
              motive t

Defined in

Mathlib.NumberTheory.HeckeRing.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group