coe_mul

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.coe_mul

English

The inclusion preserves multiplication: i(xy) = i(x) i(y) for x,y ∈ S.

Русский

Включение сохраняет умножение: i(xy) = i(x) i(y) для x,y ∈ S.

LaTeX

$$$\forall x,y \in S:\ i(xy) = i(x) i(y)$$$

Lean4

protected theorem coe_mul (x y : S) : (↑(x * y) : L) = ↑x * ↑y :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru