noZeroSMulDivisors — Mathlib

English

If R acts on A and B, A is a subalgebra of B, and B has no zero-smul-divisors over R, then A also has no zero-smul-divisors over R.

Русский

Если R действует на A, A ⊆ B и у B нет нулевых делителей масштабирования, то и у A таких нулевых делителей нет.

LaTeX

$$$\text{NoZeroSmulDivisors}\;\; R\; A \Rightarrow \text{NoZeroSmulDivisors } R A $$$

Lean4

theorem noZeroSMulDivisors [SMul R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] : NoZeroSMulDivisors R A :=
  by
  refine
    Function.Injective.noZeroSMulDivisors _ (IsIntegralClosure.algebraMap_injective A R B) (map_zero _) fun _ _ => ?_
  simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc]

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