Defs

📁 Source: Mathlib/LinearAlgebra/Quotient/Defs.lean

Statistics

Metric	Count
Definitions addCommGroup, distribMulAction, distribMulAction', distribSMul, distribSMul', instInhabitedQuotient, instSMul, instSMul', instZeroQuotient, mk, module', mulAction, mulAction', smulZeroClass, smulZeroClass', hasQuotient, mkQ, quotEquivOfEq, quotientRel	19
Theorems eq, eq', forall, induction_on, instSmallQuotient, isCentralScalar, isScalarTower, mk''_eq_mk, mk'_eq_mk', mk_add, mk_eq_zero, mk_neg, mk_out, mk_smul, mk_sub, mk_surjective, mk_zero, quot_mk_eq_mk, quotientAddGroupMk_eq_mk, smulCommClass, linearMap_qext, linearMap_qext_iff, mkQ_apply, mkQ_surjective, quotEquivOfEq_mk, quot_hom_ext, quotientRel_def	27
Total	46

Submodule

Definitions

Name	Category	Theorems
hasQuotient 📖	CompOp	339 math math: Ideal.toCotangent_to_quotient_square, TopModuleCat.hom_cokerπ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, lTensor.inverse_comp_lTensor, AdicCompletion.val_sub_apply, QuotientBot.infinite, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, Module.support_quotient, Module.Presentation.cokernelSolution_var, Module.End.IsNilpotent.mapQ, annihilator_quotient, AdicCompletion.map_val_apply, covBy_iff_quot_is_simple, ModuleCat.epi_as_hom''_mkQ, Module.isTorsionBySet_quotient_set_smul, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, mapQ_apply, dualQuotEquivDualAnnihilator_apply, Quotient.mk_add, factor_mk, Module.isTorsionBySet_quotient_ideal_smul, t3_quotient_of_isClosed, Quotient.instIsBoundedSMul, quotDualCoannihilatorToDual_apply, dualPairing_apply, unique_quotient_iff_eq_top, lTensor.inverse_of_rightInverse_comp_lTensor, AdicCompletion.val_smul, AdicCompletion.incl_apply, AdicCompletion.val_smul_eq_evalₐ_smul, quotientPi_aux.map_smul, Quotient.instDiscreteMeasurableSpaceQuotient, Module.supportDim_add_length_eq_supportDim_of_isRegular, finrank_quotient_add_finrank, Module.exists_smul_eq_zero_and_mk_eq, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, Quotient.instSubsingletonQuotient, isArtinian_iff_submodule_quotient, Module.Grassmannian.rankAtStalk_eq, dualCopairing_eq, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, IsLocalRing.map_mkQ_eq, quotDualCoannihilatorToDual_nondegenerate, quotEquivOfEqBot_symm_apply, Module.Presentation.cokernel_relation, LieHom.quotKerEquivRange_toFun, QuotSMulTop.map_comp_mkQ, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, LinearMap.range_mkQ_comp, rTensor.inverse_of_rightInverse_apply, AdicCompletion.pi_apply_coe, LinearMap.exact_subtype_mkQ, Module.Presentation.cokernel_R, RingTheory.Sequence.isWeaklyRegular_iff_Fin, AdicCompletion.val_add_apply, AdicCompletion.smul_eval, rank_quotient_add_rank, Subspace.finiteDimensional_quot_dualCoannihilator_iff, ZSpan.quotientEquiv_apply_mk, Module.Presentation.cokernelSolution.isPresentation, AdicCompletion.factor_eval_eq_evalₐ, goursat, quotientQuotientEquivQuotientAux_mk, FiniteDimensional.finiteDimensional_quotient, lTensor.inverse_of_rightInverse_apply, mapQ_pow, range_mkQ, isOpenQuotientMap_mkQ, factor_eq_factor, Subspace.dualPairing_nondegenerate, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, Quotient.completeSpace, linearMap_qext_iff, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, strictMono_comap_prod_map, Quotient.equiv_symm, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, LinearMap.surjective_range_liftQ, AdicCompletion.val_sum, Ideal.pi_mkQ_surjective, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, isNoetherian_iff_submodule_quotient, Quotient.mk_sub, lTensor.inverse_apply, LinearMap.comap_leq_ker_subToSupQuotient, map_mkQ_eq_top, isArtinian_of_quotient_of_artinian, LinearMap.quotientInfEquivSupQuotient_apply_mk, KaehlerDifferential.kerTotal_mkQ_single_add, AdicCompletion.range_eval, Ideal.Quotient.smul_top, finiteQuotient_iff, AdicCompletion.val_neg_apply, Function.Exact.exact_mapQ_iff, Module.Quotient.mk_smul_mk, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, mapQ_zero, Module.Finite.quotient, AdicCompletion.transitionMap_comp_eval, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, Ideal.quotientToQuotientRangePowQuotSucc_mk, subsingleton_quotient_iff_eq_top, coe_quotEquivOfEqBot_symm, CharacterModule.intSpanEquivQuotAddOrderOf_apply, annihilator_map_mkQ_eq_colon, AdicCompletion.coe_eval, ker_liftQ_eq_bot', TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, AdicCompletion.val_mul, Quotient.mk_smul, mkQ_apply, AdicCompletion.mk_smul_mk, card_quotient_mul_card_quotient, factor_comp, Subspace.flip_quotDualCoannihilatorToDual_bijective, rank_quotient_add_rank_of_isDomain, quotEquivOfEqBot_apply_mk, IsSemisimpleModule.exists_quotient_linearEquiv_submodule, LinearMap.quotientInfEquivSupQuotient_injective, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, KaehlerDifferential.derivationQuotKerTotal_apply, AdicCompletion.transitionMap_comp_reduceModIdeal, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, dualCopairing_apply, le_comap_mkQ, LinearMap.exact_smul_id_smul_top_mkQ, Quotient.restrictScalarsEquiv_symm_mk, finite_quotient_smul, natAbs_det_equiv, AdicCompletion.smul_mk, mapQ_eq_factor, LinearMap.injective_range_liftQ_of_exact, Module.Grassmannian.finite_quotient, Module.Presentation.cokernel_var, IsLocalizedModule.toLocalizedQuotient', Ideal.quotientToQuotientRangePowQuotSucc_surjective, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, quotientPi_apply, rTensor.inverse_of_rightInverse_comp_rTensor, Subspace.quotAnnihilatorEquiv_apply, RingTheory.Sequence.isWeaklyRegular_append_iff', isNoetherian_quotient, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, isSMulRegular_quotient_iff_mem_of_smul_mem, rTensor.inverse_comp_rTensor, LinearMap.liftQ₂_mk, quotientEquivOfIsCompl_apply_mk_coe, comapMkQOrderEmbedding_eq, groupHomology.π_comp_H1Iso_hom_apply, LinearMap.quotKerEquivRange_symm_apply_image, rTensor_mkQ, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, RingTheory.Sequence.isWeaklyRegular_append_iff, Quotient.equiv_symm_apply, pi_liftQ_eq_liftQ_pi, HasRankNullity.rank_quotient_add_rank, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, IsModuleTopology.instQuot, comap_map_mkQ, ker_liftQ_eq_bot, Module.IsTorsionBySet.quotient, Quotient.instSmallQuotient, Quotient.nontrivial_of_ne_top, LinearMap.quotKerEquivRange_apply_mk, isSimpleModule_iff_quot_maximal, Ideal.annihilator_quotient, LieHom.quotKerEquivRange_invFun, isOpenMap_mkQ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, quotientEquivOfIsCompl_symm_apply, Ideal.quotientToQuotientRangePowQuotSucc_injective, finiteQuotientOfFreeOfRankEq, TensorProduct.quotTensorEquivQuotSMul_symm_mk, quotDualCoannihilatorToDual_injective, quotientPi_symm_apply, Module.jacobson_quotient_of_le, liftQ_apply, KaehlerDifferential.kerTotal_mkQ_single_mul, Quotient.isCentralScalar, AdicCompletion.val_add, isQuotientEquivQuotientPrime_iff, quotientPi_aux.map_add, Module.Presentation.cokernel_G, Module.exists_isPrincipal_quotient_of_finite, LinearMap.exact_map_mkQ_range, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, AdicCompletion.val_one, mkQ_map_self, AdicCompletion.factor_eval_liftRingHom, rank_quotient_add_rank_le, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, toLocalizedQuotient'_mk, Quotient.mk_surjective, KaehlerDifferential.kerTotal_mkQ_single_smul, topologicalAddGroup_quotient, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, TensorProduct.quotientTensorEquiv_apply_tmul_mk, QuotientTorsion.instIsTorsionFree, Quotient.isScalarTower, Module.isTorsionBySet_quotient_iff, ZSpan.quotientEquiv.symm_apply, AdicCompletion.transitionMap_map_pow, rank_quotient_le, mk_quotientEquivOfIsCompl_apply, Subspace.dualCopairing_nondegenerate, map_liftQ, piQuotientLift_single, liftQSpanSingleton_apply, Quotient.mk_neg, Ideal.pi_mkQ_rTensor, KaehlerDifferential.quotKerTotalEquiv_symm_apply, LinearMap.quotKerEquivOfSurjective_symm_apply, mapQ_mkQ, rTensor.inverse_apply, AdicCompletion.val_sub, Module.Basis.sumQuot_inr, quotientPi_aux.left_inv, RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial, AdicCompletion.val_neg, Module.isTorsionBy_quotient_iff, factor_comp_apply, quotEquivOfEq_mk, AdicCompletion.transitionMap_ideal_mk, AdicCompletion.transitionMap_map_mul, Function.Exact.linearEquivOfSurjective_apply, LinearMap.coe_quotientInfToSupQuotient, range_dualMap_mkQ_eq, groupCohomology.π_comp_H2Iso_hom_apply, finite_dualAnnihilator_iff, Representation.quotient_apply, groupCohomology.π_comp_H1Iso_hom_apply, linearIndepOn_union_iff_quotient, ker_mkQ, groupHomology.π_comp_H2Iso_hom_apply, quotientPiLift_mk, continuousSMul_quotient, mkQ_surjective, finrank_quotient_eq_sum, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, AdicCompletion.factor_evalₐ_eq_eval, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, Function.Exact.linearEquivOfSurjective_symm_apply, Module.length_quotient, Ideal.cotangentEquivIdeal_symm_apply, isSimpleModule_iff_isCoatom, AdicCompletion.eval_of, rank_quotient_add_rank_of_divisionRing, quotientPi_aux.right_inv, LinearMap.det_eq_det_mul_det, isSMulRegular_on_quot_iff_lsmul_comap_eq, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, Quotient.subsingleton_iff, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, Quotient.smulCommClass, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, Module.Grassmannian.projective_quotient, AdicCompletion.val_zero, groupHomology.π_comp_H1Iso_inv_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, AdicCompletion.mk_apply_coe, Quotient.norm_mk_le, IsLocalRing.map_mkQ_eq_top, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, RingTheory.Sequence.isWeaklyRegular_iff, mapQ_comp, goursat_surjective, AdicCompletion.transitionMap_comp_eval_apply, TensorProduct.quotTensorEquivQuotSMul_comp_mk, finrank_quotient_le, AdicCompletion.val_zero_apply, rank_quotient_eq_of_le_torsion, Module.Finite.exists_fin_quot_equiv, finrank_quotient, liftQ_mkQ, dualAnnihilator_eq_bot_iff', LinearMap.ker_le_range_iff, isSMulRegular_on_quot_iff_lsmul_comap_le, Quotient.norm_mk_lt, dualQuotEquivDualAnnihilator_symm_apply_mk, ker_liftQ, QuotientTorsion.torsion_eq_bot, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, LinearMap.ker_eq_bot_range_liftQ_iff, AdicCompletion.eval_surjective, Rep.mkQ_hom, Quotient.nontrivial_iff, AdicCompletion.transitionMap_map_one, Module.jacobson_quotient_jacobson, Subspace.quotDualCoannihilatorToDual_bijective, lTensor_mkQ, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, AdicCompletion.eval_apply, IsSemisimpleModule.quotient, Quotient.equiv_trans, KaehlerDifferential.quotKerTotalEquiv_apply, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, quotient_prod_linearEquiv, Quotient.restrictScalarsEquiv_mk, LinearMap.quotientInfEquivSupQuotient_surjective, Module.finrank_quotient_add_finrank_le, AdicCompletion.val_sum_apply, Quotient.mk_eq_zero, LinearMap.quotKerEquivOfSurjective_apply_mk, Quotient.nontrivial_of_lt_top, comap_liftQ, groupHomology.π_comp_H2Iso_inv_apply, Quotient.mk_zero, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, AdicCompletion.of_apply, Module.isTorsionBy_quotient_element_smul, Module.IsTorsionBy.quotient, piQuotientLift_mk, flip_quotDualCoannihilatorToDual_injective, Subspace.dualPairing_eq, mapQ_id, AdicCompletion.eval_comp_of, Ideal.to_quotient_square_comp_toCotangent, factor_comp_mk, Module.Basis.sumQuot_repr_inr, AdicCompletion.val_smul_apply, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, card_eq_card_quotient_mul_card, quotientQuotientEquivQuotientAux_mk_mk, LinearIndepOn.quotient_iff_union, factor_surjective, Quotient.equiv_apply, natAbs_det_basis_change, cardQuot_apply, range_liftQ, KaehlerDifferential.kerTotal_mkQ_single_algebraMap
mkQ 📖	CompOp	88 math math: Ideal.toCotangent_to_quotient_square, TopModuleCat.hom_cokerπ, lTensor.inverse_comp_lTensor, Module.Presentation.cokernelSolution_var, ModuleCat.epi_as_hom''_mkQ, factor_mk, lTensor.inverse_of_rightInverse_comp_lTensor, IsAdicComplete.mkQ_comp_lift, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, IsLocalRing.map_mkQ_eq, QuotSMulTop.map_comp_mkQ, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, LinearMap.range_mkQ_comp, LinearMap.exact_subtype_mkQ, goursat, quotientQuotientEquivQuotientAux_mk, range_mkQ, isOpenQuotientMap_mkQ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, linearMap_qext_iff, strictMono_comap_prod_map, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, Ideal.pi_mkQ_surjective, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, map_mkQ_eq_top, KaehlerDifferential.kerTotal_mkQ_single_add, ModuleCat.smulShortComplex_g, coe_quotEquivOfEqBot_symm, annihilator_map_mkQ_eq_colon, mkQ_apply, card_quotient_mul_card_quotient, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, KaehlerDifferential.derivationQuotKerTotal_apply, le_comap_mkQ, LinearMap.exact_smul_id_smul_top_mkQ, quotientPi_apply, rTensor.inverse_of_rightInverse_comp_rTensor, rTensor.inverse_comp_rTensor, comapMkQOrderEmbedding_eq, groupHomology.π_comp_H1Iso_hom_apply, LinearMap.quotKerEquivRange_symm_apply_image, rTensor_mkQ, comap_map_mkQ, isOpenMap_mkQ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, Module.jacobson_quotient_of_le, KaehlerDifferential.kerTotal_mkQ_single_mul, isQuotientEquivQuotientPrime_iff, LinearMap.exact_map_mkQ_range, mkQ_map_self, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, KaehlerDifferential.kerTotal_mkQ_single_smul, map_liftQ, Ideal.pi_mkQ_rTensor, mapQ_mkQ, range_dualMap_mkQ_eq, groupCohomology.π_comp_H2Iso_hom_apply, groupCohomology.π_comp_H1Iso_hom_apply, linearIndepOn_union_iff_quotient, ker_mkQ, groupHomology.π_comp_H2Iso_hom_apply, mkQ_surjective, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, Ideal.cotangentEquivIdeal_symm_apply, AdicCompletion.eval_of, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, AdicCompletion.mk_apply_coe, IsLocalRing.map_mkQ_eq_top, goursat_surjective, TensorProduct.quotTensorEquivQuotSMul_comp_mk, liftQ_mkQ, LinearMap.ker_le_range_iff, ker_liftQ, Rep.mkQ_hom, lTensor_mkQ, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, IsAdicComplete.StrictMono.mkQ_comp_lift, comap_liftQ, AdicCompletion.of_apply, AdicCompletion.eval_comp_of, Ideal.to_quotient_square_comp_toCotangent, factor_comp_mk, Module.Basis.sumQuot_repr_inr, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, quotientQuotientEquivQuotientAux_mk_mk, LinearIndepOn.quotient_iff_union, Module.Relations.Solution.ofQuotient_π, KaehlerDifferential.kerTotal_mkQ_single_algebraMap
quotEquivOfEq 📖	CompOp	4 math math: CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Quotient.equiv_refl, quotEquivOfEq_mk
quotientRel 📖	CompOp	11 math math: quotientRel_def, Quotient.mk'_eq_mk', Ideal.Quotient.mk_out, WittVector.quotientPEquiv_mk, Quotient.mk_out, Ideal.univ_eq_iUnion_image_add, Quotient.quot_mk_eq_mk, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, Quotient.mk''_eq_mk, UniformSpace.inseparableSetoid_ring, LieSubmodule.Quotient.is_quotient_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearMap_qext 📖	—	LinearMap.comp HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids mkQ	—	—	RingHomCompTriple.ids LinearMap.ext Quotient.induction_on LinearMap.congr_fun
linearMap_qext_iff 📖	mathematical	—	LinearMap.comp HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids mkQ	—	RingHomCompTriple.ids linearMap_qext
mkQ_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike mkQ	—	—
mkQ_surjective 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Quotient.addCommGroup Quotient.module LinearMap.instFunLike mkQ	—	—
quotEquivOfEq_mk 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike quotEquivOfEq	—	RingHomInvPair.ids
quot_hom_ext 📖	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike	—	—	LinearMap.ext Quotient.induction_on
quotientRel_def 📖	mathematical	—	quotientRel Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	QuotientAddGroup.leftRel_apply sub_eq_add_neg neg_add neg_neg neg_mem_iff AddSubgroupClass.toNegMemClass addSubgroupClass

Submodule.Quotient

Definitions

Name	Category	Theorems
addCommGroup 📖	CompOp	323 math math: Ideal.toCotangent_to_quotient_square, TopModuleCat.hom_cokerπ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, lTensor.inverse_comp_lTensor, AdicCompletion.val_sub_apply, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, Module.support_quotient, Module.Presentation.cokernelSolution_var, IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, RingTheory.Sequence.isWeaklyRegular_cons_iff', Module.End.IsNilpotent.mapQ, Submodule.annihilator_quotient, AdicCompletion.map_val_apply, covBy_iff_quot_is_simple, ModuleCat.epi_as_hom''_mkQ, RingTheory.Sequence.isWeaklyRegular_cons_iff, Module.isTorsionBySet_quotient_set_smul, Ring.coe_jacobson_quotient, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, Submodule.mapQ_apply, Submodule.dualQuotEquivDualAnnihilator_apply, mk_add, Submodule.factor_mk, Module.isTorsionBySet_quotient_ideal_smul, QuotSMulTop.equivTensorQuot_naturality, Submodule.top_eq_ofList_cons_smul_iff, Submodule.quotDualCoannihilatorToDual_apply, Submodule.dualPairing_apply, lTensor.inverse_of_rightInverse_comp_lTensor, AdicCompletion.incl_apply, AdicCompletion.val_smul_eq_evalₐ_smul, Module.supportDim_add_length_eq_supportDim_of_isRegular, Submodule.finrank_quotient_add_finrank, Module.exists_smul_eq_zero_and_mk_eq, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, isArtinian_iff_submodule_quotient, Module.Grassmannian.rankAtStalk_eq, Submodule.dualCopairing_eq, RingTheory.Sequence.isRegular_cons_iff, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, QuotSMulTop.equivTensorQuot_naturality_mk, IsLocalRing.map_mkQ_eq, Submodule.quotDualCoannihilatorToDual_nondegenerate, Submodule.quotEquivOfEqBot_symm_apply, Module.Presentation.cokernel_relation, LieHom.quotKerEquivRange_toFun, QuotSMulTop.map_comp_mkQ, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, ModN.basis_apply_eq_mkQ, LinearMap.range_mkQ_comp, rTensor.inverse_of_rightInverse_apply, AdicCompletion.pi_apply_coe, LinearMap.exact_subtype_mkQ, Module.Presentation.cokernel_R, AdicCompletion.val_add_apply, ModuleCat.smulShortComplex_X₃_isAddCommGroup, Submodule.rank_quotient_add_rank, Subspace.finiteDimensional_quot_dualCoannihilator_iff, Module.Presentation.cokernelSolution.isPresentation, AdicCompletion.factor_eval_eq_evalₐ, Submodule.goursat, Submodule.quotientQuotientEquivQuotientAux_mk, FiniteDimensional.finiteDimensional_quotient, lTensor.inverse_of_rightInverse_apply, Submodule.mapQ_pow, Submodule.range_mkQ, QuotSMulTop.map_surjective, Submodule.isOpenQuotientMap_mkQ, Submodule.factor_eq_factor, Subspace.dualPairing_nondegenerate, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, Hausdorffification.instIsHausdorff, Submodule.linearMap_qext_iff, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, Submodule.strictMono_comap_prod_map, equiv_symm, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, LinearMap.surjective_range_liftQ, AdicCompletion.val_sum, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, isNoetherian_iff_submodule_quotient, mk_sub, lTensor.inverse_apply, LinearMap.comap_leq_ker_subToSupQuotient, Submodule.map_mkQ_eq_top, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, AlgebraicClosure.instIsAlgClosureOfIsAlgebraic, isArtinian_of_quotient_of_artinian, LinearMap.quotientInfEquivSupQuotient_apply_mk, KaehlerDifferential.kerTotal_mkQ_single_add, AdicCompletion.range_eval, AdicCompletion.val_neg_apply, Function.Exact.exact_mapQ_iff, Module.Quotient.mk_smul_mk, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, Submodule.mapQ_zero, Module.Finite.quotient, AdicCompletion.transitionMap_comp_eval, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, Ideal.quotientToQuotientRangePowQuotSucc_mk, ModuleCat.smulShortComplex_g, Submodule.coe_quotEquivOfEqBot_symm, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Submodule.annihilator_map_mkQ_eq_colon, AdicCompletion.coe_eval, Submodule.ker_liftQ_eq_bot', TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, isFiniteLength_quotient_span_singleton, Submodule.mkQ_apply, Submodule.card_quotient_mul_card_quotient, Submodule.factor_comp, Subspace.flip_quotDualCoannihilatorToDual_bijective, rank_quotient_add_rank_of_isDomain, Submodule.quotEquivOfEqBot_apply_mk, IsSemisimpleModule.exists_quotient_linearEquiv_submodule, LinearMap.quotientInfEquivSupQuotient_injective, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, QuotSMulTop.equivQuotTensor_naturality, KaehlerDifferential.derivationQuotKerTotal_apply, AdicCompletion.transitionMap_comp_reduceModIdeal, Submodule.dualCopairing_apply, Submodule.le_comap_mkQ, AlgebraicClosure.instIsAlgClosure, LinearMap.exact_smul_id_smul_top_mkQ, restrictScalarsEquiv_symm_mk, Submodule.mapQ_eq_factor, LinearMap.injective_range_liftQ_of_exact, Module.Grassmannian.finite_quotient, Module.Presentation.cokernel_var, IsLocalizedModule.toLocalizedQuotient', Ideal.quotientToQuotientRangePowQuotSucc_surjective, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, Submodule.quotientPi_apply, rTensor.inverse_of_rightInverse_comp_rTensor, Subspace.quotAnnihilatorEquiv_apply, RingTheory.Sequence.isWeaklyRegular_append_iff', isNoetherian_quotient, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, rTensor.inverse_comp_rTensor, LinearMap.liftQ₂_mk, Submodule.quotientEquivOfIsCompl_apply_mk_coe, Submodule.comapMkQOrderEmbedding_eq, QuotSMulTop.map_exact, groupHomology.π_comp_H1Iso_hom_apply, LinearMap.quotKerEquivRange_symm_apply_image, rTensor_mkQ, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, RingTheory.Sequence.isWeaklyRegular_append_iff, equiv_symm_apply, Submodule.pi_liftQ_eq_liftQ_pi, HasRankNullity.rank_quotient_add_rank, Module.supportDim_quotSMulTop_succ_eq_supportDim, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, IsModuleTopology.instQuot, Submodule.comap_map_mkQ, Submodule.ker_liftQ_eq_bot, Module.IsTorsionBySet.quotient, LinearMap.quotKerEquivRange_apply_mk, isSimpleModule_iff_quot_maximal, Ideal.annihilator_quotient, LieHom.quotKerEquivRange_invFun, Submodule.isOpenMap_mkQ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, Submodule.quotientEquivOfIsCompl_symm_apply, Ideal.quotientToQuotientRangePowQuotSucc_injective, TensorProduct.quotTensorEquivQuotSMul_symm_mk, Submodule.quotDualCoannihilatorToDual_injective, Submodule.quotientPi_symm_apply, Module.jacobson_quotient_of_le, Submodule.liftQ_apply, KaehlerDifferential.kerTotal_mkQ_single_mul, AdicCompletion.val_add, Submodule.isQuotientEquivQuotientPrime_iff, Submodule.quotientPi_aux.map_add, Module.Presentation.cokernel_G, Module.supportDim_le_supportDim_quotSMulTop_succ, QuotSMulTop.equivQuotTensor_naturality_mk, Module.exists_isPrincipal_quotient_of_finite, LinearMap.exact_map_mkQ_range, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Submodule.mkQ_map_self, Module.support_quotSMulTop, AdicCompletion.factor_eval_liftRingHom, rank_quotient_add_rank_le, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Submodule.toLocalizedQuotient'_mk, KaehlerDifferential.kerTotal_mkQ_single_smul, Submodule.topologicalAddGroup_quotient, Hausdorffification.lift_comp_of, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, TensorProduct.quotientTensorEquiv_apply_tmul_mk, Submodule.QuotientTorsion.instIsTorsionFree, Module.isTorsionBySet_quotient_iff, AdicCompletion.transitionMap_map_pow, rank_quotient_le, Submodule.mk_quotientEquivOfIsCompl_apply, Subspace.dualCopairing_nondegenerate, Submodule.map_liftQ, Submodule.piQuotientLift_single, Submodule.liftQSpanSingleton_apply, mk_neg, KaehlerDifferential.quotKerTotalEquiv_symm_apply, LinearMap.quotKerEquivOfSurjective_symm_apply, Submodule.mapQ_mkQ, rTensor.inverse_apply, AdicCompletion.val_sub, Module.Basis.sumQuot_inr, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, AdicCompletion.val_neg, Module.isTorsionBy_quotient_iff, Submodule.factor_comp_apply, Submodule.quotEquivOfEq_mk, AdicCompletion.transitionMap_ideal_mk, AdicCompletion.transitionMap_map_mul, Function.Exact.linearEquivOfSurjective_apply, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, LinearMap.coe_quotientInfToSupQuotient, Submodule.range_dualMap_mkQ_eq, groupCohomology.π_comp_H2Iso_hom_apply, Hausdorffification.lift_of, QuotSMulTop.map_comp, Submodule.finite_dualAnnihilator_iff, Representation.quotient_apply, groupCohomology.π_comp_H1Iso_hom_apply, linearIndepOn_union_iff_quotient, Submodule.ker_mkQ, groupHomology.π_comp_H2Iso_hom_apply, Submodule.quotientPiLift_mk, Submodule.mkQ_surjective, Submodule.finrank_quotient_eq_sum, AdicCompletion.factor_evalₐ_eq_eval, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, Function.Exact.linearEquivOfSurjective_symm_apply, Ideal.Factors.finiteDimensional_quotient_pow, Module.length_quotient, Ideal.cotangentEquivIdeal_symm_apply, isSimpleModule_iff_isCoatom, QuotSMulTop.map_apply_mk, Module.supportDim_quotient_eq_ringKrullDim, AdicCompletion.eval_of, rank_quotient_add_rank_of_divisionRing, LinearMap.det_eq_det_mul_det, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, Module.Grassmannian.projective_quotient, groupHomology.π_comp_H1Iso_inv_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, AdicCompletion.mk_apply_coe, IsLocalRing.map_mkQ_eq_top, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, Submodule.mapQ_comp, Submodule.goursat_surjective, AdicCompletion.transitionMap_comp_eval_apply, TensorProduct.quotTensorEquivQuotSMul_comp_mk, Submodule.finrank_quotient_le, ModN.instModuleFinite, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, rank_quotient_eq_of_le_torsion, Module.Finite.exists_fin_quot_equiv, Submodule.finrank_quotient, Submodule.liftQ_mkQ, Submodule.dualAnnihilator_eq_bot_iff', QuotSMulTop.map_id, LinearMap.ker_le_range_iff, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, Submodule.ker_liftQ, Submodule.QuotientTorsion.torsion_eq_bot, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, LinearMap.ker_eq_bot_range_liftQ_iff, AdicCompletion.eval_surjective, Rep.mkQ_hom, AdicCompletion.transitionMap_map_one, Module.jacobson_quotient_jacobson, Subspace.quotDualCoannihilatorToDual_bijective, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, lTensor_mkQ, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, AdicCompletion.eval_apply, IsSemisimpleModule.quotient, equiv_trans, KaehlerDifferential.quotKerTotalEquiv_apply, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, quotient_prod_linearEquiv, RingTheory.Sequence.isRegular_cons_iff', restrictScalarsEquiv_mk, LinearMap.quotientInfEquivSupQuotient_surjective, Module.finrank_quotient_add_finrank_le, AdicCompletion.val_sum_apply, LinearMap.quotKerEquivOfSurjective_apply_mk, Submodule.comap_liftQ, groupHomology.π_comp_H2Iso_inv_apply, Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, AdicCompletion.of_apply, Module.isTorsionBy_quotient_element_smul, Module.IsTorsionBy.quotient, Submodule.piQuotientLift_mk, Submodule.flip_quotDualCoannihilatorToDual_injective, Subspace.dualPairing_eq, Submodule.mapQ_id, AdicCompletion.eval_comp_of, Ideal.to_quotient_square_comp_toCotangent, Submodule.factor_comp_mk, Module.Basis.sumQuot_repr_inr, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, Submodule.quotientQuotientEquivQuotientAux_mk_mk, LinearIndepOn.quotient_iff_union, Submodule.factor_surjective, equiv_apply, Submodule.range_liftQ, KaehlerDifferential.kerTotal_mkQ_single_algebraMap
distribMulAction 📖	CompOp	2 math math: Ideal.Quotient.smul_top, Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul
distribMulAction' 📖	CompOp	—
distribSMul 📖	CompOp	—
distribSMul' 📖	CompOp	—
instInhabitedQuotient 📖	CompOp	—
instSMul 📖	CompOp	19 math math: Submodule.quotientPi_aux.map_smul, Ideal.range_cotangentToQuotientSquare, Ideal.Quotient.tower_quotient_map_quotient, RingTheory.Sequence.isWeaklyRegular_iff_Fin, Ideal.Factors.isScalarTower, AdicCompletion.mk_smul_mk, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, AdicCompletion.transitionMap_comp_reduceModIdeal, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, AdicCompletion.smul_mk, isSMulRegular_quotient_iff_mem_of_smul_mem, IsModuleTopology.instQuot, Ideal.cotangentEquivIdeal_apply, Submodule.continuousSMul_quotient, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, Ideal.cotangentEquivIdeal_symm_apply, isSMulRegular_on_quot_iff_lsmul_comap_eq, RingTheory.Sequence.isWeaklyRegular_iff, isSMulRegular_on_quot_iff_lsmul_comap_le
instSMul' 📖	CompOp	21 math math: Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, Ideal.Quotient.isScalarTower, instIsBoundedSMul, AdicCompletion.val_smul, Ideal.Quotient.tower_quotient_map_quotient, Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, Ideal.Factors.isScalarTower, mk_smul, Submodule.instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, Ideal.Quotient.isScalarTower_of_liesOver, isCentralScalar, KaehlerDifferential.kerTotal_mkQ_single_smul, isScalarTower, Module.IsTorsionBySet.isScalarTower, Ideal.Quotient.smulCommClass', instIsScalarTowerQuotientIdealResidueField, Ideal.Quotient.smulCommClass, Ideal.KerLift.map_smul, smulCommClass, Ideal.Quotient.isScalarTower_right, AdicCompletion.val_smul_apply
instZeroQuotient 📖	CompOp	33 math math: LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, instIsBoundedSMul, Ideal.quotient_map_C_eq_zero, LinearMap.exact_subtype_mkQ, Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, MvPolynomial.quotient_map_C_eq_zero, Ideal.Quotient.eq_zero_iff_dvd, Function.Exact.exact_mapQ_iff, Ideal.Quotient.index_eq_zero, Ideal.Quotient.mk_singleton_self, Ideal.Quotient.mk_span_range, Ideal.exact_mulQuot_quotOfMul, LinearMap.exact_smul_id_smul_top_mkQ, Ideal.Quotient.eq_zero_iff_mem, QuotSMulTop.map_exact, LinearMap.exact_map_mkQ_range, ModP.preVal_zero, Submodule.piQuotientLift_single, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, AdicCompletion.val_zero, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, ModP.preVal_eq_zero, AdicCompletion.val_zero_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, Ideal.Quotient.zero_eq_one_iff, mk_eq_zero, mk_zero, Ideal.isRadical_iff_quotient_reduced, Ideal.Quotient.noZeroDivisors, Ideal.eq_zero_of_polynomial_mem_map_range, KaehlerDifferential.kerTotal_mkQ_single_algebraMap
mk 📖	CompOp	—
module' 📖	CompOp	27 math math: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, Polynomial.Monic.free_quotient, finrank_quotient_span_eq_natDegree_norm, finrank_quotient_span_eq_natDegree', KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, finrank_quotient_span_eq_natDegree, Module.Finite.quotient, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, KaehlerDifferential.derivationQuotKerTotal_apply, restrictScalarsEquiv_symm_mk, IsLocalizedModule.toLocalizedQuotient', isNoetherian_quotient, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, Polynomial.Monic.finite_quotient, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Submodule.toLocalizedQuotient'_mk, KaehlerDifferential.quotKerTotalEquiv_symm_apply, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Submodule.finrank_quotient, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, restrictScalarsEquiv_mk, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val
mulAction 📖	CompOp	—
mulAction' 📖	CompOp	—
smulZeroClass 📖	CompOp	—
smulZeroClass' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	eq' QuotientAddGroup.leftRel_apply Submodule.quotientRel_def
eq' 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	QuotientAddGroup.eq
forall 📖	—	—	—	—	Quotient.forall
induction_on 📖	—	—	—	—	Quotient.inductionOn'
instSmallQuotient 📖	mathematical	—	Small HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient	—	small_of_surjective mk_surjective
isCentralScalar 📖	mathematical	—	IsCentralScalar HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instSMul' MulOpposite	—	Quotient.ind' IsCentralScalar.op_smul_eq_smul
isScalarTower 📖	mathematical	—	IsScalarTower HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instSMul'	—	Quotient.ind' smul_assoc
mk''_eq_mk 📖	mathematical	—	Quotient.mk'' Submodule.quotientRel	—	—
mk'_eq_mk' 📖	mathematical	—	Submodule.quotientRel	—	—
mk_add 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid HasQuotient.Quotient Submodule Ring.toSemiring Submodule.hasQuotient addCommGroup	—	—
mk_eq_zero 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instZeroQuotient SetLike.instMembership Submodule.setLike	—	add_zero AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass eq'
mk_neg 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient addCommGroup	—	—
mk_out 📖	mathematical	—	Quotient.out Submodule.quotientRel	—	Quotient.out_eq
mk_smul 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instSMul'	—	—
mk_sub 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient addCommGroup	—	—
mk_surjective 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient	—	—
mk_zero 📖	mathematical	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instZeroQuotient	—	—
quot_mk_eq_mk 📖	mathematical	—	Submodule.quotientRel	—	—
quotientAddGroupMk_eq_mk 📖	mathematical	—	AddCommGroup.toAddGroup Submodule.toAddSubgroup	—	—
smulCommClass 📖	mathematical	—	SMulCommClass HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instSMul'	—	Quotient.ind' SMulCommClass.smul_comm

---

← Back to Index