Theorems · Theorem · general topology

OnePoint.map_smul

∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {L : Type u_2} [inst_2 : Field L] [inst_3 : DecidableEq L]
  (f : K →+* L) (g : GL (Fin 2) K) (c : OnePoint K),
  OnePoint.map (⇑f) (g • c) = (Matrix.GeneralLinearGroup.map f) g • OnePoint.map (⇑f) c

Defined in

Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Cited by

2 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDecidableEqFieldDecidableEq