toAffineIsometryEquiv_linearIsometryEquiv

English

The same mk' construction preserves linearIsometry equivalences when promoted to affine counterparts.

Русский

Тот же конструктор mk' сохраняет линейные эквивалентности изометрии при переходе к аффинной форме.

LaTeX

$$$$ (mk' e e' p h).linearIsometryEquiv = e'. $$$$

Lean4

@[simp]
theorem toAffineIsometryEquiv_linearIsometryEquiv : e.toAffineIsometryEquiv.linearIsometryEquiv = e :=
  by
  ext
  rfl
    -- somewhat arbitrary choice of simp direction

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