smul_mem_smul_iff_of_isUnit — Mathlib

English

If a is a unit in the monoid, then the smul equivalence holds using the unit of a.

Русский

Если a является единицей в моное, то справедлив эквивалентность smul через единицу.

LaTeX

$$$ smul\\_mem\\_smul\\_iff\\_of\\_isUnit (ha : IsUnit a) : a \\cdot p \\in a \\cdot s \\leftrightarrow p \\in s $$$

Lean4

theorem smul_mem_smul_iff_of_isUnit (ha : IsUnit a) : a • p ∈ a • s ↔ p ∈ s :=
  smul_mem_smul_iff (a := ha.unit)

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