Mathlib Map

Structures · Algebra

IsHeckeTriple

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
Shape
3 explicit arguments · adds left_le, right_le, commensurable, le_commensurator_right

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by13

Ancestors0

No ancestors.