smul_of_tower_def — Mathlib

English

The action on the subtype s is defined by r•x := ⟨r•x, witness⟩, i.e., the new element is obtained by acting on the underlying value and providing a proof it stays in s.

Русский

Действие на подтипе s задаётся как r•(x) = ⟨r•x, доказательство⟩, т.е. получаемый элемент определяется действием на базовом значении и доказательством сохранения в s.

LaTeX

$$$\\forall (s : S) (r : M) (x : s), r \\cdot x = ⟨r \\cdot x.1, motion⟩$$$

Lean4

@[to_additive]
theorem smul_of_tower_def (r : M) (x : s) : r • x = ⟨r • x, smul_one_smul N r x.1 ▸ smul_mem _ x.2⟩ :=
  rfl

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