English
Reiterates that fst respects exponentiation: for all natural n, (a^n).fst = (a.fst)^n.
Русский
Повторное утверждение: fst сохраняет степень: для всех n, (a^n).fst = (a.fst)^n.
LaTeX
$$$\\forall n \\in \\mathbb{N},\\; (a^n).\\mathrm{fst} = (a.\\mathrm{fst})^n$$$
Lean4
/-- The ring structure is inherited as the pullback under the injective map
`DoubleCentralizer.toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ` -/
instance instRing : Ring 𝓜(𝕜, A) :=
toProdMulOpposite_injective.ring _ rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
(fun _x _n => Prod.ext rfl <| MulOpposite.op_smul _ _) (fun _x _n => Prod.ext rfl <| MulOpposite.op_smul _ _)
(fun _x _n => Prod.ext rfl <| MulOpposite.op_pow _ _) (fun _ => rfl) fun _ => rfl
