English
Induction principle restated: for any P, if P holds for mk K v hv for all v ≠ 0, then P holds for every p ∈ ℙ_K(V).
Русский
Повторение принципа индукции: если P верно для всех mk K v hv с v ≠ 0, то P верно для каждого p ∈ ℙ_K(V).
LaTeX
$$$\forall P : \mathbb{P}_K(V) \to \mathrm{Prop},\ (\forall v\ (hv : v \neq 0), P(\mathrm mk\ K\ v hv)) \Rightarrow \forall p, P(p)$$$
Lean4
/-- An injective semilinear map of vector spaces induces a map on projective spaces. -/
def map {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective f) : ℙ K V → ℙ L W :=
Quotient.map' (fun v => ⟨f v, fun c => v.2 (hf (by simp [c]))⟩)
(by
rintro ⟨u, hu⟩ ⟨v, hv⟩ ⟨a, ha⟩
use Units.map σ.toMonoidHom a
dsimp at ha ⊢
erw [← f.map_smulₛₗ, ha])
