eq_smul_self_of_mem_fdo_mem_fdo — Mathlib

English

If z and g•z lie in 𝒟ᵒ, then z = g•z.

Русский

Если z и g•z лежат в 𝒟ᵒ, то z = g•z.

LaTeX

$$$ z\in 𝒟^{\circ} \land (g\cdot z)\in 𝒟^{\circ} \Rightarrow z = g\cdot z$$$

Lean4

/-- Second Fundamental Domain Lemma: if both `z` and `g • z` are in the open domain `𝒟ᵒ`,
where `z : ℍ` and `g : SL(2,ℤ)`, then `z = g • z`. -/
theorem eq_smul_self_of_mem_fdo_mem_fdo (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : z = g • z :=
  by
  obtain ⟨n, hn⟩ := exists_eq_T_zpow_of_c_eq_zero (c_eq_zero hz hg)
  rw [hn] at hg ⊢
  simp [eq_zero_of_mem_fdo_of_T_zpow_mem_fdo hz hg, one_smul]

Похожие утверждения