linear_bijective_iff — Mathlib

English

A simp-friendly version equating bijectivity of the linear part and the map itself.

Русский

Упрощённая версия эквивалентности биективности линейной части и самого отображения.

LaTeX

$$$\\text{simp lemma: } \\mathrm{Bijective}(f.linear) \\Leftrightarrow \\mathrm{Bijective}(f)$$$

Lean4

@[simp]
theorem linear_bijective_iff (f : P1 →ᵃ[k] P2) : Function.Bijective f.linear ↔ Function.Bijective f :=
  and_congr f.linear_injective_iff f.linear_surjective_iff

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