English
The construction carries a nonassociative ring structure compatible with the underlying module and scalar actions.
Русский
Конструкция обладает несовместной структурой кольца, совместимой с базовым модулем и скалярами.
LaTeX
$$$\text{NonAssocRing}(\mathrm{Unitization}(R,A))$$$
Lean4
instance instAlgebra : Algebra S (Unitization R A)
where
algebraMap := (Unitization.inlRingHom R A).comp (algebraMap S R)
commutes' := fun s x => by
induction x with
| inl_add_inr =>
change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
smul_def' := fun s x => by
induction x with
| inl_add_inr =>
change _ = inl (algebraMap S R s) * _
rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr, smul_one_mul, inl_smul, inr_smul,
smul_one_smul]
