toAffine_of_equiv — Mathlib

English

Affine coordinates respect scalar multiplication on finite triples when the scalar is a unit or appropriately treated.

Русский

Аффинные координаты сохраняют умножение на скаляры для тройок, когда скаляр является единицей или обрабатывается соответствующим образом.

LaTeX

$$$toAffine(W, u\\cdot P) = toAffine(W, P)$ for unit u$$

Lean4

theorem toAffine_of_equiv {P Q : Fin 3 → F} (h : P ≈ Q) : toAffine W P = toAffine W Q :=
  by
  rcases h with ⟨u, rfl⟩
  exact toAffine_smul Q u.isUnit

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