equivAddCircle_apply_mk — Mathlib

English

In the rescaling equivalence, the action on a representative x ∈ 𝕜 is given by x ↦ x(p⁻¹q) in 𝕜 modulo q, i.e., the image of the class of x is the class of x(p⁻¹q).

Русский

При эквивалентности масштабирования: действие на представитель x ∈ 𝕜 задано как x ↦ x(p⁻¹q) в 𝕜 по модулю q; образ класса x — это класс x(p⁻¹q).

LaTeX

$$$(\equivAddCircle(p,q))( [x]_{p} ) = [x(p^{-1}q)]_{q}$$$

Lean4

@[simp]
theorem equivAddCircle_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
    equivAddCircle p q hp hq (x : 𝕜) = (x * (p⁻¹ * q) : 𝕜) :=
  rfl

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