algebra — Mathlib

English

The fixedField of a fixingSubgroup carries a natural algebra structure over the base field.

Русский

Фиксированное поле фиксирующей подгруппы обладает естественной алгебраической структурой над основанием.

LaTeX

$$$\text{FixedField}(\text{fixingSubgroup } K) \text{ has a canonical } K\text{-algebra structure}$$$

Lean4

instance algebra : Algebra K (fixedField (fixingSubgroup K))
    where
  algebraMap :=
    { toFun x := ⟨x, fun ϕ => Subtype.mem ϕ x⟩
      map_zero' := rfl
      map_add' _ _ := rfl
      map_one' := rfl
      map_mul' _ _ := rfl }
  commutes' _ _ := mul_comm _ _
  smul_def' _ _ := rfl

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