instMulActionUnitsRingOfIntegersMixedSpace

English

There is an instance making (𝓞 K)ˣ into a MulAction on the mixed space, i.e., the action respects identity and associativity.

Русский

Существует инстанс, превращающий (𝓞 K)ˣ в MulAction на смешанном пространстве: действие сохраняет тождество и ассоциативность.

LaTeX

$$MulAction ((𝓞 K)ˣ) (mixedSpace(K)) with identity and associativity properties$$

Lean4

instance : MulAction (𝓞 K)ˣ (mixedSpace K)
    where
  one_smul := fun _ ↦ by simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]
  mul_smul := fun _ _ _ ↦ by simp_rw [unitSMul_smul, Units.coe_mul, map_mul, mul_assoc]

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