coe_comp — Mathlib

English

If e is a linear equivalence, then the map sending a derivation D to e.compDer D is itself a linear equivalence between the derivation spaces.

Русский

Если e — линейное эквивалентное отображение, то сопоставление D ↦ e.compDer D задаёт линейное эквивалентное отображение между пространствами дериваций.

LaTeX

$$$e : M \simeq N \Rightarrow e.compDer : \mathrm{Derivation}(R,A,M) \simeq \mathrm{Derivation}(R,A,N)$$$

Lean4

@[simp]
theorem coe_comp : (f.compDer D : A → N) = (f : M →ₗ[R] N).comp (D : A →ₗ[R] M) :=
  rfl

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