English
The canonical IsScalarTower instance asserts associativity of smul: (T • a) • b = T • (a • b).
Русский
Канонический экземпляр IsScalarTower утверждает ассоциативность умножения: (T • a) • b = T • (a • b).
LaTeX
$$$\text{IsScalarTower } (\mathrm{CentroidHom}(\alpha)) \; \alpha \; \alpha$$$
Lean4
/-- The canonical homomorphism from the center into the center of the centroid -/
def centerToCentroidCenter : NonUnitalSubsemiring.center α →ₙ+* Subsemiring.center (CentroidHom α)
where
toFun
z :=
{ L (z : α) with
val := ⟨L z, z.prop.left_comm, z.prop.left_assoc⟩
property := by
rw [Subsemiring.mem_center_iff]
intro g
ext a
exact map_mul_left g (↑z) a }
map_zero' := by
simp only [ZeroMemClass.coe_zero, map_zero]
exact rfl
map_add' := fun _ _ => by
dsimp
simp only [map_add]
rfl
map_mul' z₁ z₂ := by ext a; exact (z₁.prop.left_assoc z₂ a).symm
