subsingleton — Mathlib

English

If MulActionWithZero M₀ A and M₀ is subsingleton, then A is subsingleton as well.

Русский

Если MulActionWithZero M₀ A и M₀ есть свойство subsingleton, то A тоже subsingleton.

LaTeX

$$$\\text{MulActionWithZero } M_0 A \\;\\land\\; \\text{Subsingleton } M_0 \\Rightarrow \\text{Subsingleton } A$$$

Lean4

protected theorem subsingleton [MulActionWithZero M₀ A] [Subsingleton M₀] : Subsingleton A where
  allEq x y := by rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]

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