Theorems · Definition · number theory

HeckeCoset.setoid

{G : Type u_1} → [inst : Group G] → (Δ : Submonoid G) → Subgroup G → Subgroup G → Setoid ↥Δ

The setoid on Δ identifying elements with the same double coset H₁gH₂ = H₁hH₂, pulled back from DoubleCoset.setoid along the inclusion Δ ↪ G. This is an abbrev rather than a global instance: the subgroups H₁, H₂ cannot be inferred from the submonoid Δ, so this cannot participate in instance search (and a global instance would also create a Setoid diamond on ↥Δ with the left-coset setoid). The quotient map is HeckeCoset.mk.

Defined in

Mathlib.NumberTheory.HeckeRing.Defs

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

Group