mathlib3 documentation

lean-ga / for_mathlib.algebra.ring_quot

source
@[protected, instance]
def ring_quot.is_scalar_tower {S : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring R] [semiring A] [algebra S A] [algebra R A] (r : A → A → Prop) [has_smul R S] [is_scalar_tower R S A] :
is_scalar_tower R S (ring_quot r)
source
@[protected, instance]
def ring_quot.smul_comm_class {S : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring R] [semiring A] [algebra S A] [algebra R A] (r : A → A → Prop) [smul_comm_class R S A] :
smul_comm_class R S (ring_quot r)