English
The two constructions algebraMap and toAlgebra' agree in the sense that the same i is the algebra map for the new algebra structure.
Русский
Две констукции algebraMap и toAlgebra' согласованы: та же карта i является алгебраической картой для новой структуры алгебры.
LaTeX
$$$\operatorname{algebraMap}_{R,S}^{toAlgebra'} = i$.$$
Lean4
/-- Let `R` be a commutative semiring, let `A` be a semiring with a `Module R` structure.
If `(r • 1) * x = x * (r • 1) = r • x` for all `r : R` and `x : A`, then `A` is an `Algebra`
over `R`.
See note [reducible non-instances]. -/
abbrev ofModule' [CommSemiring R] [Semiring A] [Module R A] (h₁ : ∀ (r : R) (x : A), r • (1 : A) * x = r • x)
(h₂ : ∀ (r : R) (x : A), x * r • (1 : A) = r • x) : Algebra R A
where
algebraMap :=
{ toFun r := r • (1 : A)
map_one' := one_smul _ _
map_mul' r₁ r₂ := by simp only [h₁, mul_smul]
map_zero' := zero_smul _ _
map_add' r₁ r₂ := add_smul r₁ r₂ 1 }
commutes' r x := by simp [h₁, h₂]
smul_def' r x := by simp [h₁]
