RingQuot 📖 | CompData | 31 mathmath: RingQuot.add_quot, TensorAlgebra.ι_def, RingQuot.mkAlgHom_surjective, RingQuot.ringQuot_ext'_iff, RingQuot.preLift_def, RingQuot.instIsScalarTower, RingQuot.mkRingHom_def, RingQuot.idealQuotientToRingQuot_apply, RingQuot.mul_quot, RingQuot.liftAlgHom_def, RingQuot.instSMulCommClass, RingQuot.eq_lift_comp_mkRingHom, RingQuot.liftAlgHom_mkAlgHom_apply, RingQuot.lift_mkRingHom_apply, RingQuot.lift_def, RingQuot.pow_quot, RingQuot.ringQuot_ext_iff, RingQuot.zero_quot, RingQuot.mkRingHom_surjective, RingQuot.mkAlgHom_rel, RingQuot.sub_quot, RingQuot.smul_quot, RingQuot.preLiftAlgHom_def, LinearAlgebra.FreeProduct.lift_apply, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, RingQuot.one_quot, RingQuot.neg_quot, RingQuot.mkRingHom_rel, RingQuot.eq_liftAlgHom_comp_mkAlgHom, RingQuot.mkAlgHom_coe, RingQuot.ringQuotToIdealQuotient_apply
|