toLinearMapClassNNRat — Mathlib

English

Any F that is a RingHomClass between R and S yields a LinearMapClass over ℚ≥0, i.e., the structure is linear over the nonnegative rationals.

Русский

Любой F, являющийся RingHomClass между R и S, образует LinearMapClass над ℚ≥0, то есть структура линейна над неотрицательными рациональными числами.

LaTeX

$$$$ \\text{LinearMapClass } F \\mathbb{Q}_{\\ge 0} R S $$$$

Lean4

instance _root_.RingHomClass.toLinearMapClassNNRat [FunLike F R S] [RingHomClass F R S] : LinearMapClass F ℚ≥0 R S where
  map_smulₛₗ f q a := by simp [smul_def, cast_id]

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