smul — Mathlib

English

A refinement expressing the correspondence for joins and fixed fields; the fixingSubgroup of a join corresponds to the meet of subgroups, etc.

Русский

Уточнение соответствия для объединений и фиксированных полей; фиксационная подгруппа объединения соответствует пересечению подгрупп и т.п.

LaTeX

$$$ (K \sqcup L).fixingSubgroup = K.fixingSubgroup \cap L.fixingSubgroup $$$

Lean4

instance smul : SMul K (fixedField (fixingSubgroup K)) where
  smul x y := ⟨x * y, fun ϕ => by rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]⟩

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