| Name | Category | Theorems |
|---|
instAddCommGroupWithOne 📖 | CompOp | — |
instAddCommMonoidWithOne 📖 | CompOp | — |
instAddGroupWithOne 📖 | CompOp | — |
instAddMonoidWithOne 📖 | CompOp | 1 mathmath: charP
|
instCommRing 📖 | CompOp | — |
instCommSemiring 📖 | CompOp | — |
instDistrib 📖 | CompOp | — |
instIntCast 📖 | CompOp | 2 mathmath: unop_intCast, op_intCast
|
instNatCast 📖 | CompOp | 2 mathmath: op_natCast, unop_natCast
|
instNonAssocRing 📖 | CompOp | — |
instNonAssocSemiring 📖 | CompOp | 78 mathmath: Matrix.toLinearMapRight'_mul, Subsemiring.op_injective, LinearEquiv.domMulActCongrRight_symm_apply, DoubleCentralizer.nnnorm_def', CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, Subsemiring.op_eq_bot, Subsemiring.op_eq_top, Subsemiring.op_sup, Subsemiring.op_le_op_iff, Subsemiring.le_op_iff, LinearEquiv.domMulActCongrRight_apply, RingHom.toOpposite_apply, DoubleCentralizer.norm_def', Matrix.toLinearEquivRight'OfInv_symm_apply, Subsemiring.op_sInf, Subsemiring.addEquivOp_apply_coe, Subring.mopRingEquivOp_apply_coe, Subalgebra.mopAlgEquivOp_symm_apply, Subsemiring.unop_le_unop_iff, Subsemiring.unop_closure, Subsemiring.unop_eq_top, AlgHom.toRingHom_toOpposite, Subsemiring.op_iSup, Subsemiring.opEquiv_apply, Subsemiring.op_closure, Subsemiring.unop_sup, Subsemiring.op_le_iff, Subsemiring.unop_sInf, Matrix.toLinearMapRight'_mul_apply, Subalgebra.linearEquivOp_apply_coe, Subsemiring.mem_op, Subring.mopRingEquivOp_symm_apply, Subsemiring.centerToMulOpposite_symm_apply_coe, Subsemiring.addEquivOp_symm_apply_coe, Subsemiring.centerToMulOpposite_apply_coe, Subsemiring.opEquiv_symm_apply, Subsemiring.unop_injective, LinearMap.toMatrixRight'_id, Subsemiring.mopRingEquivOp_apply_coe, Subsemiring.op_inf, RingHom.op_symm_apply_apply, AlgHom.toRingHom_fromOpposite, Subsemiring.unop_inf, Subsemiring.unop_top, Subalgebra.algEquivOpMop_apply, Subsemiring.op_sSup, Matrix.toLinearMapRight'_apply, Subring.ringEquivOpMop_symm_apply_coe, Subsemiring.ringEquivOpMop_symm_apply_coe, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, AlgHom.toRingHom_unop, Matrix.toLinearEquivRight'OfInv_apply, AlgHom.toRingHom_op, Subsemiring.coe_op, Subsemiring.op_toSubmonoid, Subsemiring.unop_bot, TwoSidedIdeal.subtypeMop_apply, Subsemiring.ringEquivOpMop_apply, RingHom.fromOpposite_apply, Subsemiring.op_top, Subsemiring.unop_iInf, Subsemiring.unop_sSup, Subsemiring.unop_eq_bot, TwoSidedIdeal.subtypeMop_injective, RingHom.op_apply_apply, Matrix.toLinearMapRight'_one, Subsemiring.mopRingEquivOp_symm_apply, Subalgebra.mopAlgEquivOp_apply_coe, Subalgebra.algEquivOpMop_symm_apply_coe, Subring.ringEquivOpMop_apply, Subsemiring.unop_toSubmonoid, Subsemiring.unop_iSup, Subsemiring.mem_unop, Subsemiring.coe_unop, LinearMap.toMatrixRight'_comp, Subsemiring.op_iInf, DoubleCentralizer.toProdMulOppositeHom_apply, Subsemiring.op_bot
|
instNonUnitalCommRing 📖 | CompOp | — |
instNonUnitalCommSemiring 📖 | CompOp | — |
instNonUnitalNonAssocRing 📖 | CompOp | 13 mathmath: TwoSidedIdeal.mem_op_iff, IsSimpleRing.instMulOpposite, TwoSidedIdeal.opOrderIso_symm_apply, associator_op, TwoSidedIdeal.opOrderIso_apply, instIsTopologicalRingMulOpposite, TwoSidedIdeal.op_ringCon, NonUnitalSubring.centerToMulOpposite_symm_apply_coe, TwoSidedIdeal.coe_unop, TwoSidedIdeal.coe_op, TwoSidedIdeal.mem_unop_iff, NonUnitalSubring.centerToMulOpposite_apply_coe, TwoSidedIdeal.unop_ringCon
|
instNonUnitalNonAssocSemiring 📖 | CompOp | 9 mathmath: CStarMatrix.norm_def', NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, NonUnitalRingHom.fromOpposite_apply, NonUnitalRingHom.op_symm_apply_apply, NonUnitalRingHom.toOpposite_apply, NonUnitalRingHom.op_apply_apply, NonUnitalSubsemiring.centerToMulOpposite_apply_coe, instIsTopologicalSemiringMulOpposite
|
instNonUnitalRing 📖 | CompOp | — |
instNonUnitalSemiring 📖 | CompOp | 1 mathmath: instStarOrderedRing
|
instRing 📖 | CompOp | 88 mathmath: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, CategoryTheory.preadditiveCoyonedaObj_map, Subring.coe_unop, Subring.addEquivOp_apply_coe, Subring.coe_op, CategoryTheory.Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, isLinearTopology_iff_hasBasis_open_twoSidedIdeal, Subring.op_le_op_iff, Subring.le_op_iff, Subring.unop_injective, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full, FormalMultilinearSeries.ofScalarsSum_op, Subring.op_sup, Subring.mopRingEquivOp_apply_coe, MvPowerSeries.substAlgHom_eq_aeval, Subring.op_injective, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj, Subring.unop_top, CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Subring.op_bot, MvPowerSeries.LinearTopology.instIsLinearTopologyMulOpposite, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_carrier, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d, CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj, Subring.op_sSup, Subring.centerToMulOpposite_symm_apply_coe, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, Subring.op_top, Subring.mopRingEquivOp_symm_apply, NormedSpace.exp_op, Subring.op_iInf, Subalgebra.unop_toSubring, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, Subring.op_sInf, Subring.unop_eq_top, Subring.unop_sInf, CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, IsLinearTopology.instMulOpposite, Subring.mem_unop, Subring.mem_op, CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective, Subring.unop_le_unop_iff, Subring.centerToMulOpposite_apply_coe, Subring.unop_inf, Subring.op_eq_bot, Subring.op_le_iff, Subring.op_toSubsemiring, Subring.unop_eq_bot, Subring.unop_bot, Subalgebra.op_toSubring, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, Subring.ringEquivOpMop_symm_apply_coe, Subring.unop_closure, Subring.unop_toSubsemiring, Subring.unop_sup, CategoryTheory.Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Subring.op_iSup, IsSemisimpleRing.instMulOpposite, IsCentralScalar.isLinearTopology_iff, CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective, Subring.opEquiv_apply, CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Subring.op_closure, Subring.opEquiv_symm_apply, isSemisimpleRing_mulOpposite_iff, Subring.op_inf, Subring.unop_iInf, PowerSeries.substAlgHom_eq_aeval, Subring.unop_iSup, CategoryTheory.Mat.equivalenceSingleObjInverse_map, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, CategoryTheory.preadditiveCoyonedaObj_obj_carrier, Subring.op_eq_top, CategoryTheory.preadditiveCoyonedaObj_obj_isModule, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_str, CategoryTheory.preservesLimits_preadditiveCoyonedaObj, CategoryTheory.additive_coyonedaObj, Subring.unop_sSup, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc, isLinearTopology_iff_hasBasis_twoSidedIdeal, Subring.ringEquivOpMop_apply, CategoryTheory.preadditiveCoyoneda_obj, CategoryTheory.preadditiveCoyonedaObj_obj_isAddCommGroup, NormedSpace.exp_unop, CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, Subring.addEquivOp_symm_apply_coe, FormalMultilinearSeries.ofScalarsSum_unop
|
instSemiring 📖 | CompOp | 285 mathmath: CliffordAlgebra.unop_reverseOp, HasStrictFDerivAt.fun_mul', AlgEquiv.moduleEndSelfOp_apply_apply, Subalgebra.op_toSubsemiring, AlgEquiv.opOp_apply, hasStrictFDerivAt_list_prod_finRange', TrivSqZeroExt.lift_inlAlgHom_inrHom, instRankConditionMulOpposite, Matrix.toLinearMapRight'_mul, Subalgebra.mem_op, Polynomial.opRingEquiv_op_monomial, TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst, AlgEquiv.toOpposite_apply, fderivWithin_fun_pow', Submodule.comap_op_mul, Subalgebra.op_sSup, TensorAlgebra.toTrivSqZeroExt_ι, LinearMap.ext_ring_op_iff, LinearEquiv.domMulActCongrRight_symm_apply, AlgEquiv.toOpposite_symm_apply, Submodule.comap_op_pow, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, TrivSqZeroExt.inv_inl, Subalgebra.op_sInf, Subalgebra.op_bot, AlgEquiv.op_apply_apply, TrivSqZeroExt.inv_one, instIsDomain, Submodule.LinearDisjoint.op, MonoidAlgebra.opRingEquiv_single, CliffordAlgebra.op_reverse, HasStrictFDerivAt.mul', ExteriorAlgebra.toTrivSqZeroExt_comp_map, Polynomial.leadingCoeff_opRingEquiv, TrivSqZeroExt.fstHom_comp_map, fderiv_fun_pow', AlgHom.mulLeftRightMatrix.inv_comp, TrivSqZeroExt.fst_exp, LinearEquiv.domMulActCongrRight_apply, TrivSqZeroExt.map_inr, Subalgebra.unop_sup, MonoidAlgebra.opRingEquiv_symm_apply, AlgHom.op_apply_apply, AlgEquiv.toAlgHom_op, AlgEquiv.toLinearEquiv_toOpposite, AddMonoidAlgebra.opRingEquiv_symm_single, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, AddMonoidAlgebra.opRingEquiv_symm_apply, Matrix.toLinearEquivRight'OfInv_symm_apply, DualNumber.inv_eps, HasStrictFDerivAt.list_prod', AlgHom.toLinearMap_toOpposite, NormMulClass.toNormSMulClass_op, TrivSqZeroExt.fst_invOf, algebraMap_apply, Submodule.map_unop_mul, rank_lt_rank_dual', Polynomial.opRingEquiv_op_C, Subalgebra.mopAlgEquivOp_symm_apply, Subalgebra.op_adjoin, AlgHom.opComm_symm_apply_apply, TrivSqZeroExt.map_comp_inlAlgHom, fderiv_mul_const', TrivSqZeroExt.eq_smul_exp_of_ne_zero, TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf, AlgEquiv.op_apply_symm_apply, Subalgebra.unop_top, TrivSqZeroExt.isNilpotent_inr, AlgEquiv.mopMatrix_apply, AlgHom.toRingHom_toOpposite, Subalgebra.op_inf, TrivSqZeroExt.mul_left_eq_one, Subalgebra.coe_op, TrivSqZeroExt.snd_exp, DualNumber.isNilpotent_iff_eps_dvd, TrivSqZeroExt.map_comp_inrHom, fderiv_pow', Algebra.TensorProduct.opAlgEquiv_apply, lift_rank_lt_rank_dual', AlgHom.opComm_apply_apply, RingEquiv.moduleEndSelfOp_apply, IsAzumaya.mulLeftRight_comp_congr, TrivSqZeroExt.inr_mul_inr, Subalgebra.unop_bot, fderivWithin_fun_mul', hasFDerivAt_list_prod', Matrix.toLinearMapRight'_mul_apply, AlgHom.mulLeftRight_apply, Subalgebra.linearEquivOp_apply_coe, IsAzumaya.bij, fderiv_mul', AlgEquiv.opComm_apply_apply, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, Submodule.map_unop_pow, instIsTorsionFreeMulOpposite, Polynomial.opRingEquiv_op_X, DualNumber.exists_mul_left_or_mul_right, invariantBasisNumber_iff, TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf, MonoidAlgebra.opRingEquiv_symm_single, hasFDerivWithinAt_pow', TrivSqZeroExt.isNilpotent_inl_iff, TrivSqZeroExt.mul_inv_cancel, RingEquiv.moduleEndSelf_apply, TrivSqZeroExt.inv_mul_cancel, fderivWithin_mul_const', hasFDerivAt_list_prod_finRange', Submodule.equivOpposite_apply, TrivSqZeroExt.invOf_eq_inv, Subalgebra.unop_sSup, AlgEquiv.toRingEquiv_unop, TwoSidedIdeal.mem_asIdealOpposite, Subalgebra.unop_le_unop_iff, Submodule.map_op_pow, CliffordAlgebra.reverseOpEquiv_opComm, HasFDerivWithinAt.mul_const', IsTopologicalSemiring.toOppositeIsModuleTopology, fderiv_pow_ring', AlgEquiv.toRingEquiv_opOp, rank_dual_eq_card_dual_of_aleph0_le_rank', DoubleCentralizer.instIsCentralScalar, Subalgebra.unop_iInf, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, TrivSqZeroExt.inv_inv, AlgEquiv.op_symm_apply_symm_apply, TrivSqZeroExt.exp_def, HasFDerivAt.fun_pow', Subalgebra.unop_inf, HasMFDerivWithinAt.mul', IsAzumaya.coe_tensorEquivEnd, AlgHom.fromOpposite_apply, ExteriorAlgebra.toTrivSqZeroExt_ι, TrivSqZeroExt.snd_invOf, QuaternionAlgebra.coe_starAe, LinearMap.toMatrixRight'_id, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, instInvariantBasisNumberMulOpposite, Subalgebra.mem_unop, Subalgebra.op_top, Subalgebra.unop_adjoin, Algebra.TensorProduct.opAlgEquiv_symm_apply, hasStrictFDerivAt_pow', Subalgebra.op_iInf, LieSubmodule.Quotient.isCentralScalar, Polynomial.opRingEquiv_symm_C_mul_X_pow, fderiv_fun_mul', TrivSqZeroExt.liftEquivOfComm_apply, Subalgebra.op_le_iff, AlgHom.toRingHom_fromOpposite, Polynomial.opRingEquiv_symm_monomial, Submodule.linearDisjoint_op, CliffordAlgebra.toBaseChange_comp_reverseOp, TrivSqZeroExt.isUnit_inv_iff, Polynomial.support_opRingEquiv, TrivSqZeroExt.inv_neg, Submodule.map_op_mul, hasStrictFDerivAt_list_prod_attach', MeasureTheory.Lp.instIsCentralScalar, Matrix.scalar_comm_iff, TrivSqZeroExt.sndHom_comp_map, AddMonoidAlgebra.opRingEquiv_single, TrivSqZeroExt.map_comp_map, Subalgebra.algEquivOpMop_apply, AlgEquiv.opComm_apply_symm_apply, TrivSqZeroExt.algebraMap_eq_inl, AlgHom.toLinearMap_fromOpposite, AlgEquiv.toRingEquiv_op, AddMonoidAlgebra.opRingEquiv_apply, Matrix.toLinearMapRight'_apply, HasFDerivWithinAt.pow', HasFDerivAt.list_prod', hasFDerivAt_pow', DualNumber.commute_eps_left, Submodule.map_unop_one, TrivSqZeroExt.isUnit_inr_iff, Polynomial.coeff_opRingEquiv, instIsOrderedRing, AlgEquiv.toAlgHom_unop, AlgEquiv.moduleEndSelf_apply_apply, Quaternion.coe_starAe, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, TrivSqZeroExt.isUnit_or_isNilpotent_of_isMaximal_isNilpotent, AlgHom.toRingHom_unop, Subalgebra.op_iSup, Algebra.IsCentral.instMulOpposite, Subalgebra.op_sup, TrivSqZeroExt.snd_map, AlgEquiv.moduleEndSelfOp_symm_apply, DualNumber.commute_eps_right, CliffordAlgebra.reverseOp_ι, Matrix.transposeAlgEquiv_apply, Matrix.toLinearEquivRight'OfInv_apply, TrivSqZeroExt.fst_map, HasFDerivAt.pow', HasStrictFDerivAt.pow', AlgHom.toRingHom_op, Subalgebra.unop_toSubsemiring, Subalgebra.coe_unop, TrivSqZeroExt.liftEquivOfComm_symm_apply_coe, HasStrictFDerivAt.mul_const', AlgEquiv.opComm_symm_apply_apply, AlgEquiv.moduleEndSelf_symm_apply, Submodule.comap_unop_pow, AlgEquiv.opComm_symm_apply_symm_apply, fderivWithin_list_prod', HasFDerivWithinAt.fun_mul', Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, TrivSqZeroExt.algebraMap_eq_inlHom, Subalgebra.opEquiv_symm_apply, fderivWithin_pow_ring', Algebra.TensorProduct.opAlgEquiv_tmul, AlgEquiv.mopMatrix_symm_apply, TwoSidedIdeal.subtypeMop_apply, Subalgebra.linearEquivOp_symm_apply_coe, AlgEquiv.toRingEquiv_toOpposite, HasFDerivWithinAt.fun_pow', Matrix.transposeAlgEquiv_symm_apply, Polynomial.opRingEquiv_symm_C, TrivSqZeroExt.map_inl, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, HasFDerivAt.mul_const', HasStrictFDerivAt.fun_pow', AlgEquiv.op_symm_apply_apply, DualNumber.lift_op_smul, TrivSqZeroExt.mul_right_eq_one, Submodule.equivOpposite_symm_apply, Polynomial.natDegree_opRingEquiv, Submodule.comap_unop_one, Submodule.mulMap_op, hasStrictFDerivAt_list_prod', TwoSidedIdeal.subtypeMop_injective, TrivSqZeroExt.inv_zero, Ring.uniformContinuousConstSMul_op, DualNumber.eps_mul_eps, ContinuousLinearMap.isCentralScalar, Polynomial.opRingEquiv_op_C_mul_X_pow, TrivSqZeroExt.isUnit_inl_iff, TrivSqZeroExt.isUnit_iff_isUnit_fst, Matrix.toLinearMapRight'_one, HasFDerivWithinAt.mul', Submodule.comap_op_one, AlgHom.toOpposite_apply, DualNumber.snd_mul, TrivSqZeroExt.isUnit_or_isNilpotent, Submodule.map_op_one, fderivWithin_mul', RestrictScalars.isCentralScalar, Subalgebra.le_op_iff, TrivSqZeroExt.mul_inv_rev, Matrix.scalar_commute_iff, Algebra.TensorProduct.opAlgEquiv_symm_tmul, Subalgebra.mopAlgEquivOp_apply_coe, fderiv_list_prod', HasMFDerivAt.mul', Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, Subalgebra.algEquivOpMop_symm_apply_coe, AlgHom.op_symm_apply_apply, AlgEquiv.opOp_symm_apply, CliffordAlgebra.reverseOpEquiv_apply, HasFDerivAt.fun_mul', LieSubalgebra.instIsCentralScalarSubtypeMem, MonoidAlgebra.opRingEquiv_apply, HasFDerivAt.mul', hasFDerivAt_list_prod_attach', rankCondition_iff, Subalgebra.op_le_op_iff, Matrix.op_smul_eq_vecMul, Polynomial.opRingEquiv_symm_X, LinearMap.toMatrixRight'_comp, TrivSqZeroExt.inv_inr, IsLinearTopology.hasBasis_right_ideal, Submodule.comap_unop_mul, TensorProduct.instIsCentralScalar, DualNumber.isNilpotent_eps, Subalgebra.opEquiv_apply, TrivSqZeroExt.eq_smul_exp_of_invertible, TrivSqZeroExt.map_id, AlgHom.mulLeftRightMatrix.comp_inv, RingEquiv.moduleEndSelfOp_symm_apply, IsAzumaya.AlgHom.mulLeftRight_bij, HasFDerivWithinAt.list_prod', Subalgebra.unop_iSup, Subalgebra.unop_sInf, TwoSidedIdeal.coe_mop_smul, fderivWithin_pow'
|