linearIndependent_algHom_toLinearMap'

English

A variant of linear independence after restricting scalars shows independence preserved under scalar changes.

Русский

Вариант сохранения независимости после ограничения скаляров.

LaTeX

$$$\\mathrm{linearIndependent_algHom_toLinearMap'}$$$

Lean4

theorem linearIndependent_algHom_toLinearMap' (K M L) [CommRing K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L]
    [Algebra K L] [NoZeroSMulDivisors K L] : LinearIndependent K (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L) :=
  (linearIndependent_algHom_toLinearMap K M L).restrict_scalars' K

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