smul_eq — Mathlib

English

For any P ∈ Fin 3 → R and unit u, the quotient representatives of u • P and P are equal, i.e., (⟦u • P⟧) = ⟦P⟧ in the Jacobian's quotient representation.

Русский

Для любого P ∈ Fin 3 → R и единицы u эквивалентные классы u • P и P совпадают: ⟦u • P⟧ = ⟦P⟧ в представлении Джейкобия.

LaTeX

$$⟦u • P⟧ = ⟦P⟧$$

Lean4

@[simp]
theorem smul_eq (P : Fin 3 → R) {u : R} (hu : IsUnit u) : (⟦u • P⟧ : PointClass R) = ⟦P⟧ :=
  Quotient.eq.mpr <| smul_equiv P hu

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