hom_ext — Mathlib

English

Linear maps out of IndV are equal if they agree on all induced generators IndV.mk.

Русский

Линейные отображения из IndV равны, если совпадают на всех порождающих элементов IndV.mk.

LaTeX

$$IndV.hom_ext: (f,g : IndV φ ρ →ₗ[k] B) → (∀ h, f ∘ₗ IndV.mk φ ρ h = g ∘ₗ IndV.mk φ ρ h) → f = g$$

Lean4

@[ext]
theorem hom_ext {f g : IndV φ ρ →ₗ[k] B} (hfg : ∀ h : H, f ∘ₗ IndV.mk φ ρ h = g ∘ₗ IndV.mk φ ρ h) : f = g :=
  Coinvariants.hom_ext <| TensorProduct.ext <| Finsupp.lhom_ext' fun h => LinearMap.ext_ring <| hfg h

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