toLinearEquiv_ofLinearEquiv — Mathlib

English

Same as above: the linear part of the upgraded equivalence recovers the original linear equivalence.

Русский

То же самое: линейная часть обновлённой эквивалентности восстанавливает исходное линейное эквивалентное отображение.

LaTeX

$$$ \\text{(same as 439)} $$$

Lean4

@[simp]
theorem toLinearEquiv_ofLinearEquiv : toLinearEquiv (ofLinearEquiv l map_one map_mul) = l :=
  rfl

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