hom_ext — Mathlib

English

For a linear map f and a compatibility hf with respect to ρ and τ, the equation map ρ τ f hf ∘ mk ρ = mk τ ∘ f holds.

Русский

Для линейного отображения f и условия совместимости hf выполняется равенство.

LaTeX

$$$\mathrm{map}_{\rho,\tau} f\, hf \circ mk_\rho = mk_\tau \circ f$$$

Lean4

@[ext high]
theorem hom_ext {f g : Coinvariants ρ →ₗ[k] W} (H : f ∘ₗ mk ρ = g ∘ₗ mk ρ) : f = g :=
  Submodule.linearMap_qext _ H

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