instNoZeroDivisors — Mathlib

English

If M is a nontrivial free module, the rank of SymmetricAlgebra R M equals the lift of the maximum of rank_R(M) and aleph_0.

Русский

Если M ненулевой свободный модуль, ранг SymmetricAlgebra R M равен подъему максимума между рангом M и aleph_0.

LaTeX

$$$[\text{Nontrivial } M] [\text{Module.Free } R M] \Rightarrow \operatorname{rank}_R(\operatorname{Sym}_R M) = \operatorname{lift}(\max(\operatorname{rank}_R M, \aleph_0)).$$$

Lean4

/-- The `SymmetricAlgebra` of a free module over a commutative semiring with no zero-divisors has
no zero-divisors. -/
instance instNoZeroDivisors [NoZeroDivisors R] [Module.Free R M] : NoZeroDivisors (SymmetricAlgebra R M) :=
  have ⟨⟨_, b⟩⟩ := ‹Module.Free R M›
  (equivMvPolynomial b).toMulEquiv.noZeroDivisors

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