English
The AlgEquiv version of piCongrRight is defined by taking the product of ring equivalences coordinatewise.
Русский
Версия AlgEquiv для piCongrRight задаётся как произведение эквивалентностей кольца по каждой координате.
LaTeX
$$$ \\text{piCongrRight} (e) : (\\Pi i, A_1 i) \\simeq_{R} (\\Pi i, A_2 i) $$$
Lean4
/-- `R`-algebra homomorphism between the function spaces `ι → A` and `ι → B`, induced by an
`R`-algebra homomorphism `f` between `A` and `B`. -/
@[simps]
protected def compLeft (f : A →ₐ[R] B) (ι : Type*) : (ι → A) →ₐ[R] ι → B :=
{ f.toRingHom.compLeft ι with
toFun := fun h ↦ f ∘ h
commutes' := fun c ↦ by
ext
exact f.commutes' c }
