Theorems · Definition · number theory

Subgroup.strictPeriods

{R : Type u_1} → [inst : Ring R] → Subgroup (GL (Fin 2) R) → AddSubgroup R

For a subgroup 𝒢 of GL(2, R), this is the additive group of x : R such that [1, x; 0, 1] ∈ 𝒢.

Defined in

Mathlib.NumberTheory.ModularForms.Cusps

Cited by

63 results in Mathlib

Foundations

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

Assumes

Ring