mulRothNumber_map_mul_right — Mathlib

English

Roth number is preserved under right embedding by a scalar: mulRothNumber(s.map mulRightEmbedding a) = mulRothNumber(s).

Русский

Число Рота сохраняется при правом отображении через умножение на скаляр: mulRothNumber(множество.map mulRightEmbedding a) = mulRothNumber(множество).

LaTeX

$$$mulRothNumber(s.map\ (mulRightEmbedding\ a)) = mulRothNumber(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem mulRothNumber_map_mul_right : mulRothNumber (s.map <| mulRightEmbedding a) = mulRothNumber s := by
  rw [← mulLeftEmbedding_eq_mulRightEmbedding, mulRothNumber_map_mul_left s a]

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