Theorems · Inductive type · number theory

IsHeckeTriple

{G : Type u_1} → [inst : Group G] → Submonoid G → Subgroup G → Subgroup G → Prop

A Hecke triple (H₁, Δ, H₂): the compatibility conditions on a submonoid Δ and a pair of subgroups H₁, H₂ of G making the double cosets H₁\Δ/H₂ finite unions of left cosets: both subgroups are contained in Δ, they are commensurable, and Δ commensurates them. The classical Hecke pair (H, Δ) of [Shimura][shimura1971], Chapter 3, is the diagonal case IsHeckeTriple Δ H H.

Defined in

Mathlib.NumberTheory.HeckeRing.Defs

Cited by

14 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Group