AlgHom.equalizerRestrictScalars_apply
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
variable {R S A B : Type u} [CommRing R] [CommRing S] [CommRing A] [CommRing B]
[Algebra R A] [Algebra R S] [Algebra R B]
namespace AlgebraLean source · statement
lemma _root_.AlgHom.equalizerRestrictScalars_apply [Algebra S A] [Algebra S B]
[IsScalarTower R S A] [IsScalarTower R S B]
(f g : A →ₐ[S] B) (x) :
AlgHom.equalizerRestrictScalars R f g x = x