coe_toIntLinearMap_map — Mathlib

English

Equality of map_coe to additive map underlying the linear map.

Русский

Равенство map_coe и соответствующего аддитивного отображения линейного отображения.

LaTeX

$$map f p = map f p$$

Lean4

@[simp]
theorem _root_.AddMonoidHom.coe_toIntLinearMap_map {A A₂ : Type*} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂)
    (s : AddSubgroup A) : (AddSubgroup.toIntSubmodule s).map f.toIntLinearMap = AddSubgroup.toIntSubmodule (s.map f) :=
  rfl

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