English
If R, A have a faithful SMul action and A is an R-algebra with IsScalarTower R A A, then for any n ∈ ℕ with [NeZero (n:R)], the element n in A is nonzero: NeZero (n:A).
Русский
Если R и A имеют пристрастующее к себе действие и A — R-алгебра, и существует связанная тензорная башня, то для любого натурального n, не равного нулю в R, образ n в A также не равен нулю.
LaTeX
$$$\operatorname{NeZero}(n : A).$$$
Lean4
theorem _root_.NeZero.of_faithfulSMul (R A : Type*) [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A]
[FaithfulSMul R A] (n : ℕ) [NeZero (n : R)] : NeZero (n : A) :=
NeZero.nat_of_injective (f := ringHomEquivModuleIsScalarTower.symm ⟨_, ‹_›⟩) <|
(faithfulSMul_iff_injective_smul_one R A).mp ‹_›
