| Name | Category | Theorems |
|---|
includeLeft π | CompOp | 37 mathmath: lift_comp_includeLeft, includeLeft_map_center_le, MvPolynomial.universalFactorizationMap_comp_map, Subalgebra.LinearDisjoint.include_range, Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct, algEquivIncludeRange_symm_tmul, linearEquivIncludeRange_toLinearMap, includeLeft_apply, includeLeft_bijective, map_ker, CommRingCat.coproductCocone_inl, productMap_left, includeLeft_injective, CommAlgCat.fst_unop_hom, CommAlgCat.binaryCofan_inl, comm_comp_includeRight, comm_comp_includeLeft, linearEquivIncludeRange_symm_tmul, algEquivIncludeRange_tmul, map_range, ext_iff, algEquivIncludeRange_toAlgHom, polyEquivTensor_apply, Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, linearEquivIncludeRange_symm_toLinearMap, lmul'_comp_includeLeft, algEquivIncludeRange_symm_toAlgHom, liftEquiv_symm_apply_coe, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, Ideal.map_includeLeft_eq, rTensor_ker, map_comp_includeLeft, CommRingCat.coproductCocone_ΞΉ, lift_includeLeft_includeRight, linearEquivIncludeRange_tmul, includeLeft_surjective, closure_range_union_range_eq_top
|
includeLeftRingHom π | CompOp | 13 mathmath: CommRingCat.pushoutCocone_inl, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, includeLeftRingHom_comp_algebraMap, CommRingCat.isPushout_tensorProduct, algebraMap_def, AlgebraicGeometry.pullbackSpecIso_inv_fst, AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc, AlgebraicGeometry.pullbackSpecIso_hom_fst, ringHom_ext_iff, AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc, includeLeftRingHom_apply, MvPolynomial.universalFactorizationMapPresentation_jacobian, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
|
includeRight π | CompOp | 64 mathmath: Ideal.comap_fiberIsoOfBijectiveResidueField_apply, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, MvPolynomial.universalFactorizationMap_comp_map, Subalgebra.LinearDisjoint.include_range, algEquivIncludeRange_symm_tmul, includeRight_apply, linearEquivIncludeRange_toLinearMap, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, mem_adjoin_map_integralClosure_of_isStandardEtale, CommRingCat.pushoutCocone_inr, Ideal.map_includeRight_eq, AlgebraicGeometry.pullbackSpecIso_inv_snd, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, map_ker, includeRight_map_center_le, algebraMap_eq_includeRight, includeLeftRingHom_comp_algebraMap, CommRingCat.isPushout_tensorProduct, CommRingCat.coproductCocone_inr, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, includeRight_injective, lift_comp_includeRight, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, includeRight_bijective, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, lmul'_comp_includeRight, CommAlgCat.snd_unop_hom, MonoidAlgebra.tensorEquiv_tmul, comm_comp_includeRight, comm_comp_includeLeft, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, linearEquivIncludeRange_symm_tmul, algEquivIncludeRange_tmul, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, map_range, map_comp_includeRight, AddMonoidAlgebra.tensorEquiv_tmul, ext_iff, algEquivIncludeRange_toAlgHom, lTensor_ker, linearEquivIncludeRange_symm_toLinearMap, lift_comp_includeRight', algEquivIncludeRange_symm_toAlgHom, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, CommAlgCat.binaryCofan_inr, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, MvPolynomial.universalFactorizationMap_freeMonic, map_restrictScalars_comp_includeRight, liftEquiv_symm_apply_coe, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, includeRight_surjective, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, RingHom.SurjectiveOnStalks.baseChange', productMap_right, ringHom_ext_iff, AlgebraicGeometry.pullbackSpecIso_hom_snd, CommRingCat.coproductCocone_ΞΉ, lift_includeLeft_includeRight, linearEquivIncludeRange_tmul, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct, MvPolynomial.universalFactorizationMapPresentation_jacobian, closure_range_union_range_eq_top, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc
|
instAddCommGroupWithOne π | CompOp | 1 mathmath: intCast_def
|
instAddCommMonoidWithOne π | CompOp | 3 mathmath: Bialgebra.comul_natCast, natCast_def', natCast_def
|
instAlgebra π | CompOp | 191 mathmath: Subalgebra.mulMap_comm, Bialgebra.comulAlgHom_apply, algEquivOfLinearEquivTripleTensorProduct_apply, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, includeLeft_map_center_le, MvPolynomial.universalFactorizationMap_comp_map, Subalgebra.LinearDisjoint.include_range, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', CommAlgCat.braiding_hom_hom, mapOfCompatibleSMul_surjective, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, PolyEquivTensor.right_inv, Algebra.FormallyUnramified.lmul_elem, instLiesOverFiberOfIsPrime, AlgebraicGeometry.diagonal_SpecMap, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, Subalgebra.mulMap_toLinearMap, AlgHom.mulLeftRightMatrix.inv_comp, BialgCat.associator_def, comm_comp_map_apply, PolyEquivTensor.toFunAlgHom_apply_tmul, Subalgebra.comm_trans_rTensorBot, Subalgebra.mulMap_map_comp_eq, algEquivIncludeRange_symm_tmul, leftComm_tmul, includeRight_apply, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, linearEquivIncludeRange_toLinearMap, Matrix.toAlgEquiv_kroneckerStarAlgEquiv, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, lid_tmul, mem_adjoin_map_integralClosure_of_isStandardEtale, CommRingCat.pushoutCocone_inr, Ideal.map_includeRight_eq, AlgebraicGeometry.pullbackSpecIso_inv_snd, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, Bialgebra.TensorProduct.comulAlgHom_def, map_ker, includeRight_map_center_le, productMap_left_apply, algebraMap_eq_includeRight, Subalgebra.lTensorBot_one_tmul, AlgebraicGeometry.pullbackSpecIso_hom_base, productMap_left, Subalgebra.mulMap_bot_left_eq, includeLeftRingHom_comp_algebraMap, productMap_apply_tmul, KaehlerDifferential.End_equiv_aux, lmul'_apply_tmul, TensorProduct.gradedComm_algebraMap, CommRingCat.isPushout_tensorProduct, CommAlgCat.binaryCofan_pt, Bialgebra.TensorProduct.assoc_tmul, Matrix.kroneckerAlgEquiv_apply, CommRingCat.coproductCocone_inr, polyEquivTensor_symm_apply_tmul, IsAzumaya.mulLeftRight_comp_congr, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, MvPolynomial.finitePresentation_universalFactorizationMap, HopfAlgCat.associator_def, includeRight_injective, AlgHom.mulLeftRight_apply, lmul'_comp_map, IsAzumaya.bij, lift_comp_includeRight, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, Bialgebra.comul_algebraMap, Subalgebra.mulMap'_surjective, TensorProduct.isPushout, leftComm_toLinearEquiv, MvPolynomial.finite_universalFactorizationMap, coe_polyEquivTensor'_symm, MvPolynomial.universalFactorizationMapPresentation_map, coe_polyEquivTensor', includeRight_bijective, AlgCat.hom_inv_leftUnitor, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, productMap_range, productMap_eq_comp_map, lmul'_comp_includeRight, AlgCat.hom_hom_leftUnitor, MvPolynomial.universalFactorizationMapPresentation_relation, Subalgebra.rTensorBot_tmul_one, IsAzumaya.coe_tensorEquivEnd, CommAlgCat.binaryCofan_inl, MonoidAlgebra.tensorEquiv_tmul, TensorProduct.Algebra.linearMap_comp_mul', comm_comp_includeRight, matrixEquivTensor_apply_single, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, comm_comp_includeLeft, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, matrixEquivTensor_apply_symm, Subalgebra.mulMap_bot_right_eq, linearEquivIncludeRange_symm_tmul, algEquivIncludeRange_tmul, MatrixEquivTensor.left_inv, Subalgebra.lTensorBot_symm_apply, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, map_range, map_comp_includeRight, MvPolynomial.ker_evalβHom_universalFactorizationMap, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, CommAlgCat.braiding_inv_hom, AddMonoidAlgebra.tensorEquiv_tmul, ext_iff, algEquivIncludeRange_toAlgHom, Derivation.tensorProductTo_mul, comm_symm_tmul, Subalgebra.linearDisjoint_iff_injective, BialgHomClass.map_comp_comulAlgHom, PolyEquivTensor.left_inv, Subalgebra.lTensorBot_tmul, productMap_right_apply, Bialgebra.TensorProduct.lid_toAlgEquiv, Matrix.kroneckerAlgEquiv_symm_apply, polyEquivTensor_apply, Subalgebra.LinearDisjoint.val_mulMap_tmul, algebraMap_apply', Subalgebra.mulMap_range, Subalgebra.rTensorBot_symm_apply, lTensor_ker, linearEquivIncludeRange_symm_toLinearMap, MvPolynomial.pderiv_inr_universalFactorizationMap_X, AlgebraicGeometry.pullbackSpecIso_hom_base_assoc, comm_tmul, Bialgebra.TensorProduct.assoc_toCoalgEquiv, lmul'_comp_includeLeft, MatrixEquivTensor.right_inv, Bialgebra.TensorProduct.lid_toCoalgEquiv, algEquivIncludeRange_symm_toAlgHom, MvPolynomial.aeval_one_tmul, Subalgebra.comm_trans_lTensorBot, comm_comp_map, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, Matrix.toLinearEquiv_kroneckerAlgEquiv, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, CommAlgCat.binaryCofan_inr, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, MvPolynomial.universalFactorizationMap_freeMonic, MvPolynomial.universalFactorizationMapPresentation_val, AlgebraicGeometry.diagonal_Spec_map, MvPolynomial.universalFactorizationMapPresentation_Ο', map_restrictScalars_comp_includeRight, liftEquiv_symm_apply_coe, Bialgebra.TensorProduct.lid_tmul, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, includeRight_surjective, lmul'_toLinearMap, Subalgebra.val_mulMap'_tmul, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, RingHom.SurjectiveOnStalks.baseChange', Bialgebra.toLinearMap_comulAlgHom, lmul''_eq_lid_comp_mapOfCompatibleSMul, productMap_right, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Bialgebra.TensorProduct.lid_symm_apply, ringHom_ext_iff, adjoin_tmul_eq_top, Bialgebra.mul_comprβ_comul, Subalgebra.mulMap_tmul, TensorProduct.isPushout', AlgebraicGeometry.pullbackSpecIso_hom_snd, matrixEquivTensor_apply, MatrixEquivTensor.toFunAlgHom_apply, lid_toLinearEquiv, lid_symm_apply, leftComm_symm_tmul, Subalgebra.rTensorBot_tmul, Algebra.FormallyUnramified.iff_exists_tensorProduct, comm_toLinearEquiv, Bialgebra.TensorProduct.assoc_symm_tmul, Ideal.map_includeLeft_eq, Bialgebra.TensorProduct.assoc_toAlgEquiv, mapOfCompatibleSMul_tmul, CommRingCat.coproductCocone_ΞΉ, polyEquivTensor_symm_apply_tmul_eq_smul, comm_symm, lift_includeLeft_includeRight, linearEquivIncludeRange_tmul, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct, AlgHom.mulLeftRightMatrix.comp_inv, MvPolynomial.universalFactorizationMapPresentation_jacobian, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, IsAzumaya.AlgHom.mulLeftRight_bij, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', MvPolynomial.pderiv_inl_universalFactorizationMap_X, closure_range_union_range_eq_top, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc
|
instCommRing π | CompOp | 83 mathmath: CommRingCat.tensorProd_map_right, Algebra.Generators.baseChange_val, RingHom.SurjectiveOnStalks.baseChange, MvPolynomial.universalFactorizationMap_comp_map, CommRingCat.pushoutCocone_pt, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', TensorProduct.toIntegralClosure_bijective_of_isLocalization, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, AlgebraicGeometry.diagonal_SpecMap, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, Algebra.QuasiFiniteAt.baseChange, Algebra.PreSubmersivePresentation.baseChange_jacobian, Algebra.IsStandardSmoothOfRelativeDimension.baseChange, TensorProduct.toIntegralClosure_bijective_of_smooth, Algebra.IsUnramifiedAt.residueField, CommRingCat.pushoutCocone_inl, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, CommRingCat.pushoutCocone_inr, AlgebraicGeometry.pullbackSpecIso_inv_snd, Algebra.PreSubmersivePresentation.baseChange_toPresentation, CommRingCat.coproductCocone_inl, AlgebraicGeometry.pullbackSpecIso_hom_base, KaehlerDifferential.End_equiv_aux, TensorProduct.toIntegralClosure_mvPolynomial_bijective, RingHom.SurjectiveOnStalks.tensorProductMap, CommRingCat.isPushout_tensorProduct, CommAlgCat.binaryCofan_pt, KaehlerDifferential.D_apply, CommRingCat.coproductCocone_inr, AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc, MvPolynomial.finitePresentation_universalFactorizationMap, Algebra.QuasiFinite.baseChange, Algebra.FormallySmooth.instTensorProduct, Algebra.FormallyEtale.instTensorProduct, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_auxβ, MvPolynomial.finite_universalFactorizationMap, MvPolynomial.universalFactorizationMapPresentation_map, Algebra.IsStandardSmooth.baseChange, Algebra.Unramified.baseChange, AlgebraicGeometry.pullbackSpecIso_inv_fst, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, CommRingCat.coproductCocone_pt, MvPolynomial.universalFactorizationMapPresentation_relation, CommAlgCat.binaryCofan_inl, Algebra.Smooth.baseChange, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc, KaehlerDifferential.D_tensorProductTo, Algebra.FormallyUnramified.base_change, CommRingCat.coproductCoconeIsColimit_desc, AlgebraicGeometry.pullbackSpecIso_hom_fst, TensorProduct.toIntegralClosure_injective_of_flat, RingHom.Finite.tensorProductMap, Algebra.Etale.baseChange, AlgebraicGeometry.pullbackSpecIso_hom_base_assoc, AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc, AlgebraicGeometry.pullbackSpecIso_inv_fst', MvPolynomial.universalFactorizationMapPresentation_algebra_smul, Matrix.det_kroneckerTMul, CommAlgCat.binaryCofan_inr, MvPolynomial.universalFactorizationMapPresentation_val, AlgebraicGeometry.diagonal_Spec_map, MvPolynomial.universalFactorizationMapPresentation_Ο', RingHom.SurjectiveOnStalks.baseChange', Derivation.liftKaehlerDifferential_apply, Algebra.Presentation.baseChange_relation, KaehlerDifferential.DLinearMap_apply, AlgebraicGeometry.pullbackSpecIso_hom_fst', MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Algebra.instIsStandardEtaleTensorProduct, Algebra.WeaklyQuasiFiniteAt.baseChange, AlgebraicGeometry.pullbackSpecIso_hom_snd, Algebra.EssFiniteType.baseChange, CommRingCat.coproductCocone_ΞΉ, AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc, Algebra.PreSubmersivePresentation.baseChange_ring, Algebra.Presentation.baseChange_toGenerators, MvPolynomial.universalFactorizationMapPresentation_jacobian, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc
|
instCommSemiring π | CompOp | 39 mathmath: PrimeSpectrum.preimageEquivFiber_symm_apply_coe, MvPolynomial.rTensorAlgEquiv_apply, IsLocalization.mk'_tmul, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, IsLocalization.Away.tensorRight, TensorProduct.isPushout, MvPolynomial.rTensorAlgHom_toLinearMap, MvPolynomial.universalFactorizationMapPresentation_map, PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux, MvPolynomial.universalFactorizationMapPresentation_relation, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, MvPolynomial.coeff_rTensorAlgHom_tmul, PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable, MvPolynomial.ker_evalβHom_universalFactorizationMap, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, IsLocalization.Away.tensor, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, IsLocalization.tmul_mk', MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, Algebra.instIsStandardOpenImmersionTensorProduct, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, IsLocalization.tensorRight, IsLocalization.tensor, PrimeSpectrum.continuous_tensorProductTo, algEquivIncludeRange_symm_toAlgHom, MvPolynomial.aeval_one_tmul, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, MvPolynomial.universalFactorizationMapPresentation_val, MvPolynomial.universalFactorizationMapPresentation_Ο', PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, TensorProduct.isPushout', MvPolynomial.universalFactorizationMapPresentation_jacobian, MvPolynomial.rTensorAlgHom_apply_eq
|
instMul π | CompOp | 23 mathmath: Algebra.FormallyUnramified.one_tmul_mul_elem, Matrix.kroneckerTMulStarAlgEquiv_symm_apply, Algebra.FormallyUnramified.finite_of_free_aux, piRightHom_mul, RingHom.SurjectiveOnStalks.exists_mul_eq_tmul, algEquivIncludeRange_symm_tmul, SemiconjBy.tmul, LinearMap.map_mul_of_map_mul_tmul, tmul_mul_tmul, Matrix.kroneckerTMulStarAlgEquiv_apply, kroneckerTMulLinearEquiv_mul, Bialgebra.comul_mul, Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem, Commute.tmul, MatrixEquivTensor.invFun_smul, linearEquivIncludeRange_symm_tmul, Derivation.tensorProductTo_mul, PolyEquivTensor.invFun_monomial, Matrix.mul_kroneckerTMul_mul, Matrix.kroneckerStarAlgEquiv_apply, Algebra.FormallyUnramified.iff_exists_tensorProduct, Matrix.kroneckerStarAlgEquiv_symm_apply, MvPolynomial.universalFactorizationMapPresentation_jacobian
|
instNonAssocRing π | CompOp | β |
instNonAssocSemiring π | CompOp | 5 mathmath: includeLeftRingHom_comp_algebraMap, algebraMap_def, ringHom_ext_iff, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, includeLeftRingHom_apply
|
instNonUnitalNonAssocRing π | CompOp | β |
instNonUnitalNonAssocSemiring π | CompOp | 8 mathmath: sMulCommClass_right, isScalarTower_right, LinearMap.mulRight_tmul, LinearMap.mulLeft_tmul, TensorProduct.map_convMul_map, LinearMap.mul'_tensor, Bialgebra.mul_comprβ_comul, TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm
|
instNonUnitalRing π | CompOp | β |
instNonUnitalSemiring π | CompOp | β |
instOneTensorProduct π | CompOp | 13 mathmath: GradedTensorProduct.auxEquiv_one, GradedTensorProduct.auxEquiv_symm_one, kroneckerTMulLinearEquiv_one, TensorProduct.gradedComm_one, TensorProduct.gradedMul_one, piRightHom_one, Bialgebra.comul_one, Matrix.one_kroneckerTMul_one, TensorProduct.one_gradedMul, GradedTensorProduct.of_one, GradedTensorProduct.of_symm_one, one_def, MvPolynomial.universalFactorizationMapPresentation_jacobian
|
instRing π | CompOp | 31 mathmath: intCast_def', BialgCat.rightUnitor_def, HopfAlgCat.rightUnitor_def, Algebra.IsIntegral.tensorProduct, HopfAlgCat.tensorObj_instRing, BialgCat.associator_def, BialgCat.whiskerLeft_def, HopfAlgCat.whiskerLeft_def, IsPurelyInseparable.exists_pow_mem_range_tensorProduct, Algebra.IsAlgebraic.tensorProduct, KaehlerDifferential.End_equiv_aux, HopfAlgCat.whiskerRight_def, KaehlerDifferential.D_apply, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal, HopfAlgCat.associator_def, BialgCat.tensorHom_def, Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem, BialgCat.whiskerRight_def, KaehlerDifferential.submodule_span_range_eq_ideal, BialgCat.tensorObj_def, HopfAlgCat.tensorHom_def, IsIntegral.tmul, TensorProduct.tmul_of_gradedMul_of_tmul, KaehlerDifferential.span_range_eq_ideal, IsAlgebraic.tmul, HopfAlgCat.leftUnitor_def, KaehlerDifferential.DLinearMap_apply, BialgCat.leftUnitor_def, IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar, Algebra.FormallyUnramified.iff_exists_tensorProduct, closure_range_union_range_eq_top
|
instSemiring π | CompOp | 384 mathmath: congr_trans, exists_fg_and_mem_baseChange, CliffordAlgebra.toBaseChange_reverse, Subalgebra.mulMap_comm, Bialgebra.comulAlgHom_apply, algEquivOfLinearEquivTripleTensorProduct_apply, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right, instSMulCommClassTensorProduct, lift_comp_includeLeft, RingHom.SurjectiveOnStalks.baseChange, prodRight_tmul_fst, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, MvPolynomial.rTensorAlgEquiv_apply, AlgCat.hom_inv_associator, includeLeft_map_center_le, MvPolynomial.universalFactorizationMap_comp_map, Subalgebra.LinearDisjoint.include_range, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', CommAlgCat.braiding_hom_hom, Algebra.IsPushout.equiv_symm_algebraMap_left, Bialgebra.TensorProduct.map_toAlgHom, Polynomial.fiberEquivQuotient_tmul, congr_symm_apply, TensorProduct.toIntegralClosure_bijective_of_isLocalization, mapOfCompatibleSMul_surjective, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, PolyEquivTensor.right_inv, Algebra.FormallyUnramified.lmul_elem, instLiesOverFiberOfIsPrime, MonoidAlgebra.tensorEquiv.invFun_tmul, AlgebraicGeometry.diagonal_SpecMap, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, prodRight_symm_tmul, tensorTensorTensorComm_symm, map_comp, AlgCat.hom_inv_rightUnitor, Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct, Bialgebra.TensorProduct.counitAlgHom_def, algebraMap_apply, CliffordAlgebra.equivBaseChange_symm_apply, instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap, Subalgebra.mulMap_toLinearMap, piScalarRight_tmul, KaehlerDifferential.isScalarTower', AlgHom.mulLeftRightMatrix.inv_comp, BialgCat.associator_def, Module.endTensorEndAlgHom_apply, comm_comp_map_apply, PolyEquivTensor.toFunAlgHom_apply_tmul, IsPurelyInseparable.exists_pow_mem_range_tensorProduct, assoc_tmul, Subalgebra.comm_trans_rTensorBot, Subalgebra.mulMap_map_comp_eq, KaehlerDifferential.ideal_fg, map_tmul, TensorProduct.toIntegralClosure_bijective_of_smooth, Algebra.instIsReducedTensorProductOfIsAlgebraicOfIsGeometricallyReduced, Algebra.isGeometricallyReduced_iff, algEquivIncludeRange_symm_tmul, leftComm_tmul, includeRight_apply, CliffordAlgebra.ofBaseChange_toBaseChange, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, linearEquivIncludeRange_toLinearMap, Matrix.toAlgEquiv_kroneckerStarAlgEquiv, Bialgebra.TensorProduct.map_toCoalgHom, CliffordAlgebra.toBaseChange_comp_ofBaseChange, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, lid_tmul, Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv, tensorTensorTensorComm_symm_tmul, TensorProduct.Algebra.smul_def, mem_adjoin_map_integralClosure_of_isStandardEtale, includeLeft_apply, Ideal.Fiber.lift_residueField_surjective, CliffordAlgebra.toBaseChange_comp_involute, right_algebraMap_apply, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, CommRingCat.pushoutCocone_inr, Ideal.map_includeRight_eq, includeLeft_bijective, AlgebraicGeometry.pullbackSpecIso_inv_snd, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, AlgCat.hom_hom_associator, MonoidAlgebra.scalarTensorEquiv_tmul, Bialgebra.TensorProduct.comulAlgHom_def, PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field, map_ker, AddMonoidAlgebra.tensorEquiv.invFun_tmul, includeRight_map_center_le, productMap_left_apply, instSMulCommClassTensorProduct_1, algebraMap_eq_includeRight, CommRingCat.coproductCocone_inl, Subalgebra.lTensorBot_one_tmul, productMap_left, Subalgebra.mulMap_bot_left_eq, includeLeftRingHom_comp_algebraMap, productMap_apply_tmul, Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct, AlgHom.coe_tensorEqualizer, TensorProduct.toIntegralClosure_mvPolynomial_bijective, lmul'_apply_tmul, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, includeLeft_injective, RingHom.SurjectiveOnStalks.tensorProductMap, algEquivOfLinearEquivTensorProduct_apply, PrimeSpectrum.mem_image_comap_basicOpen, TensorProduct.gradedComm_algebraMap, CommRingCat.isPushout_tensorProduct, opAlgEquiv_apply, Algebra.FiniteType.baseChangeAux_surj, LinearMap.tensorProductEnd_apply, Bialgebra.TensorProduct.assoc_tmul, Matrix.kroneckerAlgEquiv_apply, CommRingCat.coproductCocone_inr, polyEquivTensor_symm_apply_tmul, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal, IsAzumaya.mulLeftRight_comp_congr, algebraMap_def, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, HopfAlgCat.associator_def, includeRight_injective, MvPolynomial.tensorEquivSum_one_tmul_C, AlgHom.mulLeftRight_apply, commRight_tmul, lmul'_comp_map, IsAzumaya.bij, lift_comp_includeRight, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, MonoidAlgebra.tensorEquiv_symm_single, map_id, Bialgebra.comul_algebraMap, AlgCat.hom_hom_rightUnitor, isField_of_isAlgebraic, congr_toLinearEquiv, Subalgebra.mulMap'_surjective, leftComm_toLinearEquiv, congr_apply, toLinearEquiv_tensorTensorTensorComm, MvPolynomial.rTensorAlgHom_toLinearMap, coe_polyEquivTensor'_symm, Subbimodule.coe_mk, MvPolynomial.universalFactorizationMapPresentation_map, MvPolynomial.algebraTensorAlgEquiv_symm_X, Matrix.kroneckerTMulAlgEquiv_symm_apply, coe_polyEquivTensor', includeRight_bijective, AlgCat.hom_inv_leftUnitor, liftEquiv_apply, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, not_isField_of_transcendental, productMap_range, Bialgebra.TensorProduct.rid_toAlgEquiv, productMap_eq_comp_map, CliffordAlgebra.ofBaseChange_tmul_ΞΉ, rid_tmul, lmul'_comp_includeRight, Algebra.pushoutDesc_apply, cancelBaseChange_tmul, map_comp_id, AlgCat.hom_hom_leftUnitor, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left, MvPolynomial.universalFactorizationMapPresentation_relation, congr_refl, Subbimodule.coe_toSubbimoduleInt, Subalgebra.rTensorBot_tmul_one, map_surjective, IsAzumaya.coe_tensorEquivEnd, AlgHom.tensorEqualizerEquiv_apply, MonoidAlgebra.tensorEquiv_tmul, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, TensorProduct.Algebra.linearMap_comp_mul', comm_comp_includeRight, CliffordAlgebra.toBaseChange_ofBaseChange, matrixEquivTensor_apply_single, cancelBaseChange_symm_tmul, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, MvPolynomial.coeff_rTensorAlgHom_tmul, comm_comp_includeLeft, Subbimodule.coe_toSubbimoduleNat, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, assoc_toLinearEquiv, assoc_symm_tmul, opAlgEquiv_symm_apply, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, matrixEquivTensor_apply_symm, Bialgebra.TensorProduct.map_tmul, Subalgebra.mulMap_bot_right_eq, linearEquivIncludeRange_symm_tmul, algEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_finiteType, MatrixEquivTensor.left_inv, CliffordAlgebra.toBaseChange_comp_reverseOp, PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable, Subalgebra.lTensorBot_symm_apply, Algebra.Etale.exists_subalgebra_fg, KaehlerDifferential.submodule_span_range_eq_ideal, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, map_range, tmul_pow, map_comp_includeRight, MvPolynomial.ker_evalβHom_universalFactorizationMap, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, Subalgebra.tmul_mem_baseChange, CommAlgCat.braiding_inv_hom, Algebra.Smooth.exists_finiteType, Algebra.IsPushout.equiv_tmul, AddMonoidAlgebra.tensorEquiv_tmul, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, CommAlgCat.associator_inv_hom, tensorTensorTensorComm_toLinearEquiv, ext_iff, KaehlerDifferential.D_tensorProductTo, algEquivIncludeRange_toAlgHom, AddMonoidAlgebra.tensorEquiv_symm_single, Derivation.tensorProductTo_mul, comm_symm_tmul, MonoidAlgebra.scalarTensorEquiv_symm_single, Subbimodule.coe_toSubmodule, quotIdealMapEquivTensorQuot_symm_tmul, PolyEquivTensor.invFun_monomial, Subalgebra.linearDisjoint_iff_injective, Subbimodule.coe_toSubmodule', isNilpotent_tensor_residueField_iff, BialgHomClass.map_comp_comulAlgHom, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, CommRingCat.coproductCoconeIsColimit_desc, piRight_tmul, PolyEquivTensor.left_inv, CliffordAlgebra.equivBaseChange_apply, Subalgebra.lTensorBot_tmul, MvPolynomial.tensorEquivSum_X_tmul_X, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, TensorProduct.toIntegralClosure_injective_of_flat, MvPolynomial.algebraTensorAlgEquiv_symm_map, productMap_right_apply, Bialgebra.TensorProduct.lid_toAlgEquiv, MvPolynomial.tensorEquivSum_C_tmul_one, Subbimodule.coe_baseChange, Matrix.kroneckerAlgEquiv_symm_apply, algHomOfLinearMapTensorProduct_apply, polyEquivTensor_apply, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, Subalgebra.LinearDisjoint.val_mulMap_tmul, right_isScalarTower, algebraMap_apply', Algebra.TensorProduct.commRight_symm_tmul, Subalgebra.mulMap_range, lift_tmul, RingHom.Finite.tensorProductMap, Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, Subalgebra.rTensorBot_symm_apply, Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul, lTensor_ker, linearEquivIncludeRange_symm_toLinearMap, MvPolynomial.pderiv_inr_universalFactorizationMap_X, tensorTensorTensorComm_tmul, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, IntermediateField.LinearDisjoint.isField_of_isAlgebraic', AddMonoidAlgebra.scalarTensorEquiv_symm_single, Algebra.baseChange_lmul, lift_comp_includeRight', Bialgebra.comul_pow, quotIdealMapEquivTensorQuot_mk, CliffordAlgebra.toBaseChange_involute, Matrix.kroneckerTMulAlgEquiv_apply, MvPolynomial.algebraTensorAlgEquiv_tmul, comm_tmul, Bialgebra.TensorProduct.assoc_toCoalgEquiv, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, KaehlerDifferential.span_range_eq_ideal, lmul'_comp_includeLeft, MatrixEquivTensor.right_inv, opAlgEquiv_tmul, rid_toLinearEquiv, Bialgebra.TensorProduct.lid_toCoalgEquiv, Bialgebra.TensorProduct.rid_symm_apply, algEquivIncludeRange_symm_toAlgHom, Subalgebra.comm_trans_lTensorBot, comm_comp_map, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, Matrix.toLinearEquiv_kroneckerAlgEquiv, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, MvPolynomial.tensorEquivSum_one_tmul_X, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, CliffordAlgebra.ofBaseChange_tmul_one, MvPolynomial.universalFactorizationMap_freeMonic, MvPolynomial.universalFactorizationMapPresentation_val, prodRight_tmul, prodRight_tmul_snd, AlgebraicGeometry.diagonal_Spec_map, MvPolynomial.universalFactorizationMapPresentation_Ο', map_restrictScalars_comp_includeRight, CommAlgCat.associator_hom_hom, liftEquiv_symm_apply_coe, Algebra.IsPushout.equiv_symm_algebraMap_right, Bialgebra.TensorProduct.rid_tmul, CliffordAlgebra.toBaseChange_ΞΉ, Bialgebra.TensorProduct.lid_tmul, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, includeRight_surjective, lmul'_toLinearMap, Subalgebra.val_mulMap'_tmul, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, RingHom.SurjectiveOnStalks.baseChange', TensorProduct.antipode_def, Bialgebra.toLinearMap_comulAlgHom, Algebra.FinitePresentation.baseChange, lmul''_eq_lid_comp_mapOfCompatibleSMul, productMap_right, Subalgebra.LinearDisjoint.isDomain, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Bialgebra.TensorProduct.lid_symm_apply, Bialgebra.TensorProduct.rid_toCoalgEquiv, AddMonoidAlgebra.scalarTensorEquiv_tmul, IntermediateField.LinearDisjoint.isField_of_forall, IntermediateField.LinearDisjoint.isDomain', MvPolynomial.algebraTensorAlgEquiv_symm_monomial, ringHom_ext_iff, toLinearMap_map, adjoin_tmul_eq_top, Bialgebra.mul_comprβ_comul, Subalgebra.mulMap_tmul, map_id_comp, piScalarRight_tmul_apply, lidOfCompatibleSMul_tmul, MvPolynomial.tensorEquivSum_X_tmul_one, AlgebraicGeometry.pullbackSpecIso_hom_snd, map_bijective, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, matrixEquivTensor_apply, MatrixEquivTensor.toFunAlgHom_apply, Algebra.QuasiFinite.instIsArtinianRingFiber, opAlgEquiv_symm_tmul, IntermediateField.LinearDisjoint.isDomain, lid_toLinearEquiv, Algebra.FiniteType.baseChange, IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar, lid_symm_apply, leftComm_symm_tmul, MvPolynomial.tensorEquivSum_C_tmul_C, Subalgebra.rTensorBot_tmul, CliffordAlgebra.ofBaseChange_comp_toBaseChange, congr_symm, Algebra.FormallyUnramified.iff_exists_tensorProduct, comm_toLinearEquiv, Bialgebra.TensorProduct.assoc_symm_tmul, Ideal.map_includeLeft_eq, Bialgebra.TensorProduct.assoc_toAlgEquiv, rid_symm_apply, rTensor_ker, map_comp_includeLeft, Subalgebra.LinearDisjoint.isDomain_of_injective, mapOfCompatibleSMul_tmul, CommRingCat.coproductCocone_ΞΉ, polyEquivTensor_symm_apply_tmul_eq_smul, AlgebraicGeometry.Proj.lift_awayMapβ_awayMapβ_surjective, IntermediateField.LinearDisjoint.isField_of_isAlgebraic, comm_symm, lift_includeLeft_includeRight, linearEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_fg, includeLeft_surjective, adjoin_one_tmul_image_eq_top, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct, AlgHom.mulLeftRightMatrix.comp_inv, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg, MvPolynomial.universalFactorizationMapPresentation_jacobian, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, IsAzumaya.AlgHom.mulLeftRight_bij, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', MvPolynomial.pderiv_inl_universalFactorizationMap_X, closure_range_union_range_eq_top, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc, MvPolynomial.rTensorAlgHom_apply_eq
|
leftAlgebra π | CompOp | 272 mathmath: CommRingCat.tensorProd_map_right, congr_trans, exists_fg_and_mem_baseChange, CliffordAlgebra.toBaseChange_reverse, Algebra.Generators.baseChange_val, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right, lift_comp_includeLeft, RingHom.SurjectiveOnStalks.baseChange, prodRight_tmul_fst, MvPolynomial.rTensorAlgEquiv_apply, AlgCat.hom_inv_associator, includeLeft_map_center_le, MvPolynomial.universalFactorizationMap_comp_map, Subalgebra.LinearDisjoint.include_range, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', Algebra.IsPushout.equiv_symm_algebraMap_left, Bialgebra.TensorProduct.map_toAlgHom, Algebra.IsIntegral.tensorProduct, Polynomial.fiberEquivQuotient_tmul, congr_symm_apply, TensorProduct.toIntegralClosure_bijective_of_isLocalization, mapOfCompatibleSMul_surjective, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, MonoidAlgebra.tensorEquiv.invFun_tmul, prodRight_symm_tmul, tensorTensorTensorComm_symm, Algebra.QuasiFiniteAt.baseChange, map_comp, AlgCat.hom_inv_rightUnitor, Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct, Bialgebra.TensorProduct.counitAlgHom_def, algebraMap_apply, Algebra.PreSubmersivePresentation.baseChange_jacobian, CliffordAlgebra.equivBaseChange_symm_apply, piScalarRight_tmul, Module.endTensorEndAlgHom_apply, comm_comp_map_apply, Algebra.IsStandardSmoothOfRelativeDimension.baseChange, IsPurelyInseparable.exists_pow_mem_range_tensorProduct, assoc_tmul, Algebra.IsAlgebraic.tensorProduct, Subalgebra.mulMap_map_comp_eq, map_tmul, TensorProduct.toIntegralClosure_bijective_of_smooth, algEquivIncludeRange_symm_tmul, Algebra.IsUnramifiedAt.residueField, CliffordAlgebra.ofBaseChange_toBaseChange, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, linearEquivIncludeRange_toLinearMap, Bialgebra.TensorProduct.map_toCoalgHom, CliffordAlgebra.toBaseChange_comp_ofBaseChange, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv, tensorTensorTensorComm_symm_tmul, includeLeft_apply, Ideal.Fiber.lift_residueField_surjective, CliffordAlgebra.toBaseChange_comp_involute, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, includeLeft_bijective, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, AlgCat.hom_hom_associator, MonoidAlgebra.scalarTensorEquiv_tmul, Algebra.PreSubmersivePresentation.baseChange_toPresentation, Bialgebra.TensorProduct.comulAlgHom_def, PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field, map_ker, AddMonoidAlgebra.tensorEquiv.invFun_tmul, CommRingCat.coproductCocone_inl, KaehlerDifferential.End_equiv_aux, AlgHom.coe_tensorEqualizer, TensorProduct.toIntegralClosure_mvPolynomial_bijective, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, includeLeft_injective, RingHom.SurjectiveOnStalks.tensorProductMap, algEquivOfLinearEquivTensorProduct_apply, PrimeSpectrum.mem_image_comap_basicOpen, opAlgEquiv_apply, Algebra.FiniteType.baseChangeAux_surj, LinearMap.tensorProductEnd_apply, Bialgebra.TensorProduct.assoc_tmul, AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc, IsAzumaya.mulLeftRight_comp_congr, algebraMap_def, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, MvPolynomial.tensorEquivSum_one_tmul_C, commRight_tmul, lmul'_comp_map, Algebra.QuasiFinite.baseChange, lift_comp_includeRight, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, MonoidAlgebra.tensorEquiv_symm_single, map_id, AlgCat.hom_hom_rightUnitor, Algebra.FormallySmooth.instTensorProduct, Algebra.FormallyEtale.instTensorProduct, congr_toLinearEquiv, TensorProduct.isPushout, congr_apply, toLinearEquiv_tensorTensorTensorComm, MvPolynomial.rTensorAlgHom_toLinearMap, coe_polyEquivTensor'_symm, MvPolynomial.algebraTensorAlgEquiv_symm_X, Algebra.IsStandardSmooth.baseChange, Matrix.kroneckerTMulAlgEquiv_symm_apply, coe_polyEquivTensor', Algebra.Unramified.baseChange, liftEquiv_apply, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, Bialgebra.TensorProduct.rid_toAlgEquiv, productMap_eq_comp_map, CliffordAlgebra.ofBaseChange_tmul_ΞΉ, rid_tmul, Algebra.pushoutDesc_apply, cancelBaseChange_tmul, map_comp_id, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left, MvPolynomial.universalFactorizationMapPresentation_relation, congr_refl, map_surjective, AlgHom.tensorEqualizerEquiv_apply, MonoidAlgebra.tensorEquiv_tmul, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, Algebra.Smooth.baseChange, CliffordAlgebra.toBaseChange_ofBaseChange, cancelBaseChange_symm_tmul, MvPolynomial.coeff_rTensorAlgHom_tmul, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, assoc_toLinearEquiv, assoc_symm_tmul, opAlgEquiv_symm_apply, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Bialgebra.TensorProduct.map_tmul, linearEquivIncludeRange_symm_tmul, algEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_finiteType, CliffordAlgebra.toBaseChange_comp_reverseOp, PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable, Algebra.Etale.exists_subalgebra_fg, KaehlerDifferential.submodule_span_range_eq_ideal, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, map_range, map_comp_includeRight, MvPolynomial.ker_evalβHom_universalFactorizationMap, Subalgebra.tmul_mem_baseChange, Algebra.Smooth.exists_finiteType, Algebra.IsPushout.equiv_tmul, AddMonoidAlgebra.tensorEquiv_tmul, Algebra.IsPushout.tensorProduct_tensorProduct, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, CommAlgCat.associator_inv_hom, tensorTensorTensorComm_toLinearEquiv, ext_iff, algEquivIncludeRange_toAlgHom, AddMonoidAlgebra.tensorEquiv_symm_single, IsLocalization.Away.tensor, MonoidAlgebra.scalarTensorEquiv_symm_single, quotIdealMapEquivTensorQuot_symm_tmul, Algebra.FormallyUnramified.base_change, isNilpotent_tensor_residueField_iff, BialgHomClass.map_comp_comulAlgHom, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, IsLocalization.tmul_mk', CommRingCat.coproductCoconeIsColimit_desc, piRight_tmul, CliffordAlgebra.equivBaseChange_apply, MvPolynomial.tensorEquivSum_X_tmul_X, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, TensorProduct.toIntegralClosure_injective_of_flat, MvPolynomial.algebraTensorAlgEquiv_symm_map, MvPolynomial.tensorEquivSum_C_tmul_one, algHomOfLinearMapTensorProduct_apply, polyEquivTensor_apply, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, Algebra.TensorProduct.commRight_symm_tmul, Algebra.instIsStandardOpenImmersionTensorProduct, lift_tmul, RingHom.Finite.tensorProductMap, Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, Algebra.Etale.baseChange, Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul, lTensor_ker, linearEquivIncludeRange_symm_toLinearMap, MvPolynomial.pderiv_inr_universalFactorizationMap_X, tensorTensorTensorComm_tmul, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, IsIntegral.tmul, AddMonoidAlgebra.scalarTensorEquiv_symm_single, Algebra.baseChange_lmul, lift_comp_includeRight', quotIdealMapEquivTensorQuot_mk, CliffordAlgebra.toBaseChange_involute, Matrix.kroneckerTMulAlgEquiv_apply, MvPolynomial.algebraTensorAlgEquiv_tmul, Bialgebra.TensorProduct.assoc_toCoalgEquiv, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, IsLocalization.tensor, opAlgEquiv_tmul, rid_toLinearEquiv, AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc, Bialgebra.TensorProduct.rid_symm_apply, algEquivIncludeRange_symm_toAlgHom, AlgebraicGeometry.pullbackSpecIso_inv_fst', IsAlgebraic.tmul, comm_comp_map, MvPolynomial.tensorEquivSum_one_tmul_X, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, CliffordAlgebra.ofBaseChange_tmul_one, MvPolynomial.universalFactorizationMap_freeMonic, prodRight_tmul, prodRight_tmul_snd, MvPolynomial.universalFactorizationMapPresentation_Ο', map_restrictScalars_comp_includeRight, CommAlgCat.associator_hom_hom, liftEquiv_symm_apply_coe, Algebra.IsPushout.equiv_symm_algebraMap_right, Bialgebra.TensorProduct.rid_tmul, CliffordAlgebra.toBaseChange_ΞΉ, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, Algebra.Presentation.baseChange_relation, Algebra.FinitePresentation.baseChange, lmul''_eq_lid_comp_mapOfCompatibleSMul, AlgebraicGeometry.pullbackSpecIso_hom_fst', PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Bialgebra.TensorProduct.rid_toCoalgEquiv, AddMonoidAlgebra.scalarTensorEquiv_tmul, MvPolynomial.algebraTensorAlgEquiv_symm_monomial, toLinearMap_map, Algebra.instIsStandardEtaleTensorProduct, map_id_comp, piScalarRight_tmul_apply, Algebra.WeaklyQuasiFiniteAt.baseChange, lidOfCompatibleSMul_tmul, TensorProduct.isPushout', MvPolynomial.tensorEquivSum_X_tmul_one, map_bijective, IsLocalization.tensorProduct_tensorProduct, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, opAlgEquiv_symm_tmul, Algebra.FiniteType.baseChange, IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar, MvPolynomial.tensorEquivSum_C_tmul_C, CliffordAlgebra.ofBaseChange_comp_toBaseChange, congr_symm, Bialgebra.TensorProduct.assoc_symm_tmul, Ideal.map_includeLeft_eq, Bialgebra.TensorProduct.assoc_toAlgEquiv, rid_symm_apply, rTensor_ker, map_comp_includeLeft, mapOfCompatibleSMul_tmul, Algebra.EssFiniteType.baseChange, CommRingCat.coproductCocone_ΞΉ, AlgebraicGeometry.Proj.lift_awayMapβ_awayMapβ_surjective, Algebra.PreSubmersivePresentation.baseChange_ring, lift_includeLeft_includeRight, linearEquivIncludeRange_tmul, Algebra.Smooth.exists_subalgebra_fg, includeLeft_surjective, adjoin_one_tmul_image_eq_top, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct, Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg, Algebra.Presentation.baseChange_toGenerators, MvPolynomial.pderiv_inl_universalFactorizationMap_X, closure_range_union_range_eq_top, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, MvPolynomial.rTensorAlgHom_apply_eq
|
mul π | CompOp | 4 mathmath: mul_one, one_mul, mul_assoc, mul_apply
|
rightAlgebra π | CompOp | 15 mathmath: instSMulCommClassTensorProduct, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, IsLocalization.mk'_tmul, right_algebraMap_apply, instSMulCommClassTensorProduct_1, algebraMap_eq_includeRight, IsLocalization.Away.tensorRight, commRight_tmul, TensorProduct.isPushout, right_isScalarTower, Algebra.TensorProduct.commRight_symm_tmul, IsLocalization.tensorRight, TensorProduct.isPushout', Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply
|