mem_nonZeroSMulDivisors — Mathlib

English

Let M be a type with a zero and a left action by M0, and suppose the action by m0 is regular (IsSMulRegular M m0). Then m0 is a nonzero smul divisor of M by M0, i.e., m0 ∈ nonZeroSMulDivisors M0 M.

Русский

Пусть M — множество с нулём и слева действует M0; если действие элемента m0 является регулярным (IsSMulRegular M m0), то m0 выступает ненулевым делителем по действию, то есть m0 ∈ nonZeroSMulDivisors M0 M.

LaTeX

$$IsSMulRegular\\ M\\ m_0 \\Rightarrow m_0 \\in nonZeroSMulDivisors\\ M_0\\ M$$

Lean4

theorem mem_nonZeroSMulDivisors {M : Type*} [Zero M] [MulActionWithZero M₀ M] {m₀ : M₀} (h : IsSMulRegular M m₀) :
    m₀ ∈ nonZeroSMulDivisors M₀ M := fun _ ↦ h.right_eq_zero_of_smul

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