| Name | Category | Theorems |
|---|
botEquivPUnit π | CompOp | 2 mathmath: botEquivPUnit_apply, botEquivPUnit_symm_apply
|
completeLattice π | CompOp | 464 mathmath: finrank_sup_add_finrank_inf_eq, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, AffineSubspace.direction_sup_eq_sup_direction, isFullyInvariant_iff_sSup_isotypicComponents, supIndep_torsionBySet_ideal, LinearMap.map_le_map_iff, RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule, Module.End.mem_invtSubmodule, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, MonoidAlgebra.Submodule.exists_isCompl, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LinearMap.IsProj.mem_invtSubmodule_iff, ImplicitFunctionData.isCompl_ker, mem_sup', AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, LieSubmodule.iSup_toSubmodule, LinearMap.IsIdempotentElem.commute_iff, LinearPMap.domain_supSpanSingleton, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, Ring.isField_iff_isSimpleOrder_ideal, instIsCompactlyGenerated, Ideal.sum_eq_sup, isOrtho_sup_right, mapβ_iSup_right, ClosedSubmodule.toSubmodule_sup, fst_sup_snd, Ideal.mem_sSup_of_mem, Module.End.independent_genEigenspace, LinearEquiv.map_mem_invtSubmodule_conj_iff, map_iSup, Module.End.eigenspaces_iSupIndep, mem_iSup_iff_exists_finsupp, DirectSum.IsInternal.submodule_iSupIndep, ClosedSubmodule.coe_sSup, ClosedComplemented.exists_isClosed_isCompl, mem_invtSubmodule_reflection_of_mem, RootPairing.invtRootSubmodule.bot_mem, RootPairing.invtRootSubmodule.eq_top_iff, LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, coe_sup, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, iSup_map_single_le, LinearMap.iSup_range_single, Ideal.comap_finsetInf, colon_finsetInf, LinearMap.eventually_iSup_ker_pow_eq, Representation.invtSubmodule.nontrivial_iff, smul_iSup', Module.End.mem_invtSubmodule_iff_mapsTo, isFiniteLength_iff_exists_compositionSeries, biSup_comap_subtype_eq_top, LinearMap.range_domRestrict_eq_range_iff, biSup_eq_range_dfinsupp_lsum, comap_map_sup_of_comap_le, LinearMap.span_singleton_sup_orthogonal_eq_top, IsSemisimpleModule.toComplementedLattice, fg_biSup, LieSubmodule.isCompl_toSubmodule, LinearMap.iInf_ker_proj_le_iSup_range_single, coe_isComplEquivProj_symm_apply, Ideal.smul_sup, Ideal.isPrimary_finsetInf, annihilator_iSup, neg_sup, sup_eq_range, neg_iSup, sub_mem_sup, Ideal.Filtration.sSup_N, Module.Dual.isCompl_ker_of_disjoint_of_ne_bot, Ideal.mem_sup_left, Ideal.prod_le_inf, OrderIso.setIsotypicComponents_apply, LinearMap.isCompl_range_inl_inr, mem_finset_inf, isNoetherian_iSup, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule, Ideal.iSup_eq_span, AffineSubspace.direction_affineSpan_insert, AffineSubspace.vectorSpan_union_of_mem_of_mem, RootPairing.mem_invtRootSubmodule_iff, sSup_isotypicComponents, IsLocalization.mapFrameHom_apply, submodule_eq_sSup_le_nonzero_spans, smul_sup', HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq, Subrepresentation.toSubmodule_sup, finiteDimensional_finset_sup, submoduleOf_sup_of_le, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint, iSup_mul, Ideal.IsPrime.inf_le', localized'_iSup, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, HomogeneousIdeal.toIdeal_iSupβ, Representation.invtSubmodule.coe_top, finiteDimensional_sup, dualCoannihilator_iSup_eq, LinearMap.map_coprod_prod, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, LinearMap.IsProj.isCompl, span_attach_biUnion, Ideal.mul_left_self_sup, comap_iSup_map_of_injective, mapβ_iSup_left, LinearIndependent.iSupIndep_span_singleton, LinearMap.iSup_range_single_eq_iInf_ker_proj, Algebra.TensorProduct.map_ker, map_sup, LinearMap.IsPerfectCompl.isCompl_right, Ideal.isPrimary_finset_inf, LinearMap.comap_leq_ker_subToSupQuotient, LieModule.coe_genWeightSpaceOf_zero, map_mkQ_eq_top, eq_top_of_disjoint, isOrtho_sSup_right, iSup_span, Module.End.invtSubmodule.isCompl_iff, LinearMap.quotientInfEquivSupQuotient_apply_mk, Module.End.iSup_genEigenspace_eq, iSup_dualAnnihilator_le_iInf, ClosedSubmodule.toSubmodule_iSup, sum_mem_iSup, mem_iSup_iff_exists_dfinsupp, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, span_range_eq_iSup, Ideal.IsHomogeneous.iSup, iSupIndep_iff_linearIndependent_of_ne_zero, iSup_eq_range_dfinsupp_lsum, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, IsMinimalPrimaryDecomposition.inf_eq, DFinsupp.iSup_range_lsingle, HomogeneousIdeal.toIdeal_sSup, Ideal.mul_sup, Polynomial.sup_aeval_range_eq_top_of_isCoprime, OrthogonalFamily.isInternal_iff, IsSemisimpleModule.sup, exists_compositionSeries_of_isNoetherian_isArtinian, Finsupp.supported_union, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, mul_sup, RootPairing.invtRootSubmodule.top_mem, LinearMap.sup_range_inl_inr, LinearMap.span_singleton_sup_ker_eq_top, isOrtho_iSup_left, Projectivization.independent_iff_iSupIndep, Ideal.sup_mul_right_self, comap_finsetInf, comap_sup_map_of_injective, IsLocalizedModule.localizedβFrameHom_apply, coe_finsetInf, restrictScalars_sSup, Module.End.invtSubmodule.one, PrimeSpectrum.zeroLocus_iSup, toAddSubmonoid_sSup, LinearMap.quotientInfEquivSupQuotient_injective, isSemisimpleModule_iff, smul_iSup, dualAnnihilator_sup_eq, Finsupp.isCompl_range_lmapDomain_span, sSupIndep_isotypicComponents, dualCoannihilator_sup_eq, AffineSubspace.direction_sup, fg_iSup, IsSemisimpleModule.finite_tfae, LinearPMap.domain_sSup, RootPairing.isCompl_rootSpan_ker_rootForm, inf_iSup_genEigenspace, RootPairing.corootSpan_mem_invtSubmodule_coreflection, Ideal.iSup_mul, isCompl_orthogonal_of_hasOrthogonalProjection, RootPairing.invtRootSubmodule.eq_bot_iff, Module.Basis.flag_succ, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', Module.End.isFinitelySemisimple_iff, fg_finset_sup, Ideal.isSimpleOrder, Ideal.Filtration.sup_N, sup_smul, Ideal.mem_span_singleton_sup, LieSubmodule.sup_toSubmodule, Ideal.finset_inf_span_singleton, KaehlerDifferential.kerTotal_map, DirectSum.IsInternal.isCompl, iSupIndep_iff_finset_sum_eq_imp_eq, VonNeumannAlgebra.IsIdempotentElem.mem_iff, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, Ideal.iSup_iInf_eq_top_iff_pairwise, closure_coe_iSup_map_single, Ideal.map_sup_comap_of_surjective, coe_isComplEquivProj_apply, DividedPowers.SubDPIdeal.sSup_carrier_def, IsSemisimpleModule.sSup_simples_le, mem_fullyInvariantSubmodule_iff, sInf_orthogonal, Ideal.map_sup, LinearMap.range_coprod, mul_iSup, pi_liftQ_eq_liftQ_pi, Ideal.comap_map_quotientMk, span_sSup, comap_map_mkQ, iSup_eq_span, span_iUnion, LieSubmodule.sSup_toSubmodule, inf_orthogonal, Ideal.map_iSup_comap_of_surjective, VonNeumannAlgebra.IsStarProjection.mem_iff, sum_mem_biSup, Matrix.ker_diagonal_toLin', ClosedSubmodule.mem_sup, IsMinimalPrimaryDecomposition.minimal, ClosedSubmodule.mem_iSup, Ideal.comap_map_of_surjective, IsSemisimpleModule.sSup_simples_eq_top, Ideal.quotientInfEquivQuotientProd_snd, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, restrictScalars_sup, IsDedekindDomain.inf_prime_pow_eq_prod, isSimpleModule_iff, LinearMap.eventually_isCompl_ker_pow_range_pow, LinearMap.eqOn_sup, add_mem_sup, sup_orthogonal_inf_of_hasOrthogonalProjection, Ideal.IsHomogeneous.sSup, sup_dualAnnihilator_le_inf, supIndep_torsionBy, Subspace.dualAnnihilator_iInf_eq, iSup_map_single, LinearMap.IsIdempotentElem.range_mem_invtSubmodule, mem_sSup_of_mem, smul_sup, Module.AEval.mem_mapSubmodule_symm_apply, ClosedSubmodule.toSubmodule_sSup, LinearPMap.domain_sup, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, HomogeneousIdeal.toIdeal_sup, IsLocalizedModule.localized'FrameHom_apply, isQuotientEquivQuotientPrime_iff, map_smul', isCompl_iff_disjoint, span_union, LinearMap.range_smul', small_iSup, Finsupp.disjoint_lsingle_lsingle, rank_add_le_rank_add_rank, sup_mul, Module.End.mem_invtSubmodule_symm_iff_le_map, spanRank_sup_le_sum_spanRank, Module.End.genEigenspace_top, iSup_torsionBy_eq_torsionBy_prod, LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum', RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule, set_smul_eq_iSup, LieSubmodule.sSup_toSubmodule_eq_iSup, ClosedSubmodule.mem_sSup, Polynomial.sup_ker_aeval_le_ker_aeval_mul, Module.End.span_orbit_mem_invtSubmodule, DividedPowers.isSubDPIdeal_iSup, Ideal.ofList_append, Ideal.homogeneousCore'_eq_sSup, Module.End.invtSubmodule.codisjoint_iff, OrthogonalFamily.range_linearIsometry, sup_orthogonal_of_hasOrthogonalProjection, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, isOrtho_iSup_right, LinearMap.IsIdempotentElem.isCompl, iSup_smul, mem_iSup_finset_iff_exists_sum, iSup_eq_span', Representation.invtSubmodule.top_mem, iInf_orthogonal, exists_isCompl, LinearMap.comap_eq_sup_ker_of_disjoint, ContinuousLinearMap.IsIdempotentElem.commute_iff, finite_finset_sup, finrank_add_le_finrank_add_finrank, Ideal.mem_quotient_iff_mem_sup, span_sSup', lt_sup_iff_notMem, Set.Mapsto.mem_invtSubmodule, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem, Ideal.IsMaximal.coprime_of_ne, map_iSup_comap_of_surjective, Ideal.add_eq_sup, RootPairing.coe_bot, coe_iSup_of_directed, Module.End.invtSubmodule.top_mem, IsLattice.sup, complementedLattice, AffineSubspace.sup_direction_le, Module.End.independent_maxGenEigenspace, mapβ_sup_left, sup_eq_top_iff, LinearMap.ker_sup_ker_le_ker_comp_of_commute, instIsSimpleOrderIdeal, mem_iSup_of_mem, Ideal.ofList_cons_smul, CliffordAlgebra.iSup_ΞΉ_range_eq_top, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, Ideal.mul_iSup, iSupIndep_iff_dfinsupp_lsum_injective, span_biUnion, LinearMap.coe_quotientInfToSupQuotient, RootPairing.isIrreducible_iff_invtRootSubmodule, is_simple_module_of_finrank_eq_one, map_sup_comap_of_surjective, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, LieSubmodule.iSup_toSubmodule_eq_top, isOrtho_sSup_left, RootPairing.rootSpan_mem_invtSubmodule_reflection, span_sup, Ideal.map_sSup, Ideal.quotientInfEquivQuotientProd_fst, Finsupp.supported_iUnion, OrthogonalFamily.independent, restrictScalars_iSup, LinearMap.coprod_map_prod, RootPairing.coe_top, iSupIndep_of_dfinsupp_lsum_injective, IsSimpleModule.toIsSimpleOrder, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, isArtinian_sup, Module.End.isSemisimple_iff', DirectSum.IsInternal.submodule_iSup_eq_top, mem_iSup_of_chain, mem_iSup_iff_exists_finset, TensorProduct.map_ker, Ideal.eq_inf_of_isPrime_inf, localizedβ_iSup, iSup_eq_toSubmodule_range, LinearMap.iSup_range_single_le_iInf_ker_proj, iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero, iSup_torsionBySet_ideal_eq_torsionBySet_iInf, mem_sSup_iff_exists_finset, LinearMap.disjoint_single_single, finset_inf_coe, sup_toAddSubmonoid, mem_finsetInf, LinearMap.map_eq_top_iff, isNoetherian_sup, mem_sup, LinearMap.isCompl_span_singleton_orthogonal, Ideal.multiset_prod_le_inf, Ideal.le_comap_sup, Module.End.iSup_maxGenEigenspace_eq_top, instIsModularLattice, Ideal.ofList_cons, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, ClosedSubmodule.coe_iSup, finite_iSup, exists_mem_sup, Finsupp.lsingle_range_le_ker_lapply, span_insert, Ideal.comap_map_of_surjective', isCompl_span_singleton_of_isCoatom_of_notMem, LinearMap.isCompl_of_proj, FG.sup, sSup_simples_eq_top_iff_isSemisimpleModule, Matrix.range_diagonal, mem_sSup_of_directed, Module.End.invtSubmodule.zero, OrderIso.setIsotypicComponents_symm_apply, Ideal.fst_comp_quotientInfEquivQuotientProd, Module.End.invtSubmodule.id, Ideal.span_union, LinearEquiv.map_mem_invtSubmodule_iff, ProjectiveSpectrum.zeroLocus_iSup_ideal, Ideal.IsHomogeneous.sup, dualAnnihilator_iSup_eq, rank_sup_add_rank_inf_eq, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, finite_sup, mem_biSup_iff_exists_dfinsupp, Representation.invtSubmodule.coe_bot, Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice, mem_sup_left, isSemisimpleModule_biSup_of_isSemisimpleModule_submodule, isArtinian_iSup, LinearMap.mapsTo_biSup_of_mapsTo, IsSemisimpleModule.exists_linearEquiv_dfinsupp, topologicalClosure_iSup_map_single, Ideal.radical_finset_inf, mem_sup_right, sup_set_smul, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule, sup_span, LinearPMap.supSpanSingleton_apply_mk, Ideal.mem_sup_right, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, Ideal.sup_mul, Ideal.snd_comp_quotientInfEquivQuotientProd, closedComplemented_iff_isClosed_exists_isClosed_isCompl, RootPairing.isCompl_corootSpan_ker_corootForm, map_add_le, Ideal.toIdeal_homogeneousHull_eq_iSup, mem_iSup_iff_exists_dfinsupp', covBy_span_singleton_sup, ClosedSubmodule.coe_sup, LinearIndependent.isCompl_span_image, iSupIndep_range_lsingle, Ideal.sup_mul_left_self, wcovBy_span_singleton_sup, Module.End.invtSubmodule.bot_mem, LieSubmodule.iSupIndep_toSubmodule, mem_iSup_of_directed, Module.End.mem_invtSubmodule_iff_map_le, ContinuousLinearMap.range_coprod, Ideal.mul_right_self_sup, CliffordAlgebra.evenOdd_isCompl, prod_sup_prod, Ideal.mem_iSup_of_mem, coe_scott_continuous, Module.AEval.mem_mapSubmodule_apply, Ideal.IsHomogeneous.iSupβ, Ideal.Filtration.iSup_N, iSup_toAddSubmonoid, DirectSum.isInternal_submodule_iff_isCompl, add_eq_sup, Subspace.dualAnnihilator_inf_eq, mem_sSup, Representation.mem_invtSubmodule, KaehlerDifferential.kerTotal_map', sup_toAddSubgroup, mem_invtSubmodule_reflection_iff, Ideal.map_iSup, LinearMap.IsPerfectCompl.isCompl_left, HomogeneousIdeal.toIdeal_iSup, LinearMap.quotientInfEquivSupQuotient_surjective, AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty, Ideal.span_insert, mapβ_sup_right, Module.End.invtSubmodule.disjoint_iff, Module.End.isSemisimple_iff, isOrtho_sup_left, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, isPrimary_finsetInf, LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum, DirectSum.range_coeLinearMap, mem_iSup, starProjection_tendsto_closure_iSup, iSupIndep_iff_forall_dfinsupp, comap_sup_of_injective, LinearMap.range_add_le, span_eq_iSup_of_singleton_spans, small_sup, span_iUnionβ, LinearMap.prod_eq_sup_map, Ideal.span_iUnion, LinearMap.surjective_domRestrict_iff, coe_iSup_of_chain, Finsupp.iSup_lsingle_range, Representation.invtSubmodule.bot_mem, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker, LinearMap.BilinForm.isCompl_span_singleton_orthogonal, finiteDimensional_iSup, LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top, HilbertBasis.finite_spans_dense, comap_map_eq
|
inhabited' π | CompOp | β |
instBot π | CompOp | 410 mathmath: Ideal.mem_bot, SModEq.bot, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, QuotientBot.infinite, Ideal.comap_bot_le_of_injective, bot_coe, le_annihilator_iff, PrimeSpectrum.asIdeal_bot, IsNoetherian.disjoint_partialSups_eventually_bot, subsingleton_iff_eq_bot, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, Ideal.under_bot, LieSubmodule.bot_toSubmodule, algebraicIndependent_iff_ker_eq_bot, LinearDisjoint.bot_right, mul_annihilator, smul_bot, restrictScalars_eq_bot_iff, mk_eq_bot, DirectSum.isInternal_ne_bot_iff, Ring.DimensionLEOne.eq_bot_of_lt, bot_lt_isotypicComponent, TruncatedWittVector.iInf_ker_truncate, vectorSpan_eq_bot_iff_subsingleton, AlgebraicIndependent.repr_ker, pi_univ_bot, restrictScalars_bot, Ideal.bot_lt_of_maximal, RootPairing.invtRootSubmodule.bot_mem, Ideal.isPrime_iff_bot_or_prime, Ideal.span_singleton_eq_bot, Fintype.linearIndependent_iff', exists_le_isAssociatedPrime_of_isNoetherianRing, RingHom.ker_equiv, mapβ_bot_right, PrimeSpectrum.denseRange_comap_iff_minimalPrimes, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, Ideal.jacobson_bot, Ideal.bot_pow, rank_bot, TwoSidedIdeal.bot_asIdeal, dualAnnihilator_eq_top_iff, orthogonal_eq_bot_iff, linearIndependent_iff_ker, LinearMap.iInf_ker_proj, isFiniteLength_iff_exists_compositionSeries, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, HomogeneousIdeal.eq_bot_iff, IsPrecomplete.bot, botEquivPUnit_apply, AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec, Finsupp.iInf_ker_lapply_le_bot, ker_subtype, orthogonalProjection_bot, LinearMap.ker_eq_bot, Ideal.prod_bot_bot, Ideal.isIdempotentElem_iff_eq_bot_or_top, Ideal.mul_bot, AlgEquiv.quotientBot_mk, LinearMap.ker_id, RingEquiv.quotientBot_symm_mk, LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot, groupCohomology.coboundariesβ_eq_bot_of_isTrivial, LinearMap.range_le_bot_iff, closedComplemented_bot, mem_bot, Ideal.isPrime_int_iff, smul_bot', is_bot_adic_iff, LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot, LinearMap.range_zero, OrthogonalFamily.isInternal_iff_of_isComplete, ContinuousLinearMap.iInf_ker_proj, ker_inl, IsLocalRing.maximalIdeal_eq_bot, HomogeneousIdeal.toIdeal_bot, LinearMap.isUnit_iff_ker_eq_bot, Module.Basis.flag_zero, annihilator_mul, LinearMap.bot_lt_ker_of_det_eq_zero, Ideal.eq_bot_or_top, FG.eq_bot_of_le_jacobson_smul, traceDual_top', Ideal.bot_mul, span_eq_bot, mem_annihilator', Ideal.IsHomogeneous.bot, LinearMap.BilinForm.orthogonal_eq_bot_iff, Ideal.map_mk_eq_bot_of_le, map_bot, Matrix.ker_mulVecLin_eq_bot_iff, vectorSpan_empty, IsHausdorff.iInf_pow_smul, botEquivPUnit_symm_apply, IsLocalization.coeSubmodule_bot, LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank, LinearDisjoint.linearIndependent_right_of_flat, RingEquiv.quotientBot_mk, eq_bot_of_subsingleton, Module.Flat.torsion_eq_bot, IsAdicComplete.bot, snd_map_fst, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, LinearMap.ker_toSpanSingleton, Ideal.span_singleton_zero, Module.End.eigenspace_restrict_eq_bot, LinearMap.range_eq_bot, fst_inf_snd, bot_smul, Ideal.isMaximal_iff_of_bijective, mapβ_bot_left, Ideal.primesOver_bot, Module.Basis.toDual_ker, Ideal.ramificationIdx_bot, Ideal.isRadical_bot, IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime, Ideal.radical_bot_of_noZeroDivisors, FractionalIdeal.coeToSubmodule_eq_bot, NonUnitalAlgebra.toSubmodule_bot, localizedβ_bot, bot_toAddSubmonoid, isOrtho_top_left, OrthogonalFamily.isInternal_iff, prod_eq_bot_iff, exists_compositionSeries_of_isNoetherian_isArtinian, iSupIndep.subtype_ne_bot_le_finrank, annihilator_smul, AlgHom.ker_coe_equiv, NumberField.RingOfIntegers.ker_algebraMap_eq_bot, Ideal.Quotient.mk_bijective_iff_eq_bot, dualCoannihilator_bot, Ideal.instIsTwoSidedBot, dualCoannihilator_top, LinearMap.separatingRight_iff_flip_ker_eq_bot, IsLocalization.bot_lt_comap_prime, ker_liftQ_eq_bot', LinearEquiv.eq_bot_of_equiv, annihilator_bot, span_singleton_eq_bot, IsDomain.minimalPrimes_eq_singleton_bot, Ideal.map_eq_bot_iff_of_injective, LinearMap.ker_toSpanSingleton_eq_bot_iff, baseChange_bot, Ideal.dvd_bot, Ideal.comap_bot_of_injective, top_orthogonal_eq_bot, IsLocalRing.isField_iff_maximalIdeal_eq, isSMulRegular_iff_torsionBy_eq_bot, isSimpleRing_iff_isTwoSided_imp, Matrix.ker_toLin_eq_bot, ModuleCat.ker_eq_bot_of_mono, LinearMapClass.ker_eq_bot, Ideal.isRadical_bot_iff, LinearMap.ker_eq_bot', eq_bot_of_generator_maximal_submoduleImage_eq_zero, exists_dual_map_eq_bot_of_lt_top, Ideal.map_quotient_self, bot_pow, bot_isPrincipal, iSupIndep.subtype_ne_bot_le_rank, LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot, ker_inclusion, IsHausdorff.bot, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', FractionalIdeal.coeIdeal_eq_zero', starProjection_bot, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, Ideal.isRadical_bot_of_noZeroDivisors, Ideal.isPrime_bot, MvPolynomial.zeroLocus_bot, Ideal.zero_eq_bot, finrank_eq_zero, Module.length_bot, pNilradical_eq_bot, Module.End.injOn_genEigenspace, IsSimpleModule.jacobson_eq_bot, LinearMap.hasEigenvalue_zero_tfae, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, RingHom.ker_eq_bot_iff_eq_zero, Ideal.relNorm_eq_bot_iff, IsAdicComplete.le_jacobson_bot, Ideal.map_bot, Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal, map_inr, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, Module.End.injOn_maxGenEigenspace, rank_eq_zero, Matrix.ker_toLin'_eq_bot_iff, Polynomial.jacobson_bot_of_integral_localization, transcendental_iff_ker_eq_bot, PrimeSpectrum.zeroLocus_bot, neg_bot, ker_liftQ_eq_bot, instLiesOverResidueFieldBotIdeal, map_eq_bot_iff, ArchimedeanClass.ball_top, Ideal.ramificationIdx_bot', Ideal.Filtration.bot_N, empty_set_smul, Ideal.comap_map_of_surjective, bot_colon', ProjectiveSpectrum.zeroLocus_bot, maximal_orthonormal_iff_orthogonalComplement_eq_bot, LieSubalgebra.toSubmodule_eq_bot, isOrtho_top_right, Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot, LinearMap.ker_eq_bot_of_cancel, FractionalIdeal.coeIdeal_bot, Module.eval_ker, finite_ne_bot_of_iSupIndep, associated_norm_prod_smith, LocallyConstant.ker_comapβ, Ideal.iInf_pow_eq_bot_of_isLocalRing, Finsupp.supported_empty, Module.Flat.flat_iff_torsion_eq_bot_of_isBezout, ker_subtypeL, bot_mul, AlgebraicGeometry.Scheme.default_asIdeal, Valuation.leIdeal_zero, Ideal.eq_bot_of_prime, fst_map_snd, Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot, isQuotientEquivQuotientPrime_iff, RingHom.injective_iff_ker_eq_bot, ProperCone.toPointedCone_bot, Ideal.isPrime_nat_iff, Polynomial.contentIdeal_eq_bot_iff, mkQ_map_self, Ideal.bot_isMaximal, IsArtinianRing.isNilpotent_jacobson_bot, map_zero, vectorSpan_singleton, Module.annihilator_eq_bot, dividedPowersBot_dpow_eq, Polynomial.contentIdeal_zero, PerfectRing.pNilradical_eq_bot, Ideal.instLiesOverBotOfIsPrime, map_inl, Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors, topologicalClosure_eq_top_iff, RingHom.ker_eq_comap_bot, MvPolynomial.ker_evalβ, reflection_bot, span_zero_singleton, torsionBy_one, dualAnnihilator_top, IsPrincipal.eq_bot_iff_generator_eq_zero, LinearIndependent.repr_ker, LieSubmodule.mk_eq_bot_iff, Ideal.span_eq_bot, cardQuot_bot, Ideal.smul_bot, Ideal.span_zero, Module.length_eq_coheight, AlgEquiv.quotientBot_symm_mk, Ideal.ofList_nil, LinearMap.IsProj.submodule_eq_bot_iff, IsDiscreteValuationRing.TFAE, prod_bot, FractionalIdeal.coeIdeal_eq_zero, RootPairing.coe_bot, Ideal.inertiaDeg_bot, Module.Basis.eq_bot_of_rank_eq_zero, set_smul_bot, zero_eq_bot, AffineSubspace.direction_bot, LinearMap.span_singleton_inf_orthogonal_eq_bot, basisOfPid_bot, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime, Ideal.iInf_pow_eq_bot_of_isDomain, traceDual_bot, Ideal.spanNorm_bot, RingHom.ker_coe_equiv, isOrtho_bot_right, ClosedSubmodule.toSubmodule_bot, nilradical_eq_bot_iff, finiteDimensional_bot, Ideal.prod_eq_bot_iff, LinearMap.IsProj.bot, isTorsionFree_iff_torsion_eq_bot, orthogonal_eq_top_iff, Module.End.ker_aeval_ring_hom'_unit_polynomial, LinearMap.BilinForm.orthogonal_bot, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, Ideal.span_empty, Module.ker_algebraMap_end, torsionBySet_univ, inf_orthogonal_eq_bot, LinearMap.ker_eq_bot_of_injective, bot_lt_isotypicComponents, eq_bot_of_generator_maximal_map_eq_zero, IsCoercive.ker_eq_bot, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_bot_iff, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, spanFinrank_eq_zero_iff_eq_bot, IsSemisimpleRing.jacobson_eq_bot, Module.Finite.bot, ContinuousMap.idealOfEmpty_eq_bot, Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors, IsArtinian.isSemisimpleModule_iff_jacobson, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, spanFinrank_bot, bot_orthogonal_eq_top, span_empty, pNilradical_one, LinearMap.ker_eq_bot_iff_range_eq_top, Ideal.spanNorm_eq_bot_iff, dualAnnihilator_bot, Ideal.absNorm_eq_zero_iff, spanRank_eq_zero_iff_eq_bot, LinearMap.BilinForm.orthogonal_eq_top_iff, eq_zero_of_bot_submodule, LinearMap.injective_domRestrict_iff, Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors, coe_torsion_eq_annihilator_ne_bot, FaithfulSMul.ker_algebraMap_eq_bot, IsSemisimpleModule.eq_bot_or_exists_simple_le, eq_bot_iff, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, LinearMap.BilinForm.orthogonal_top_eq_bot, Ideal.absNorm_bot, isOrtho_self, ModuleCat.mono_iff_ker_eq_bot, fg_bot, exists_dual_map_eq_bot_of_notMem, LinearMap.separatingLeft_iff_ker_eq_bot, Ring.isField_iff_maximal_bot, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, LinearMap.BilinForm.Nondegenerate.ker_eq_bot, DualNumber.ideal_trichotomy, LinearMap.trace_eq_sum_trace_restrict', finrank_bot, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, Ideal.matrix_bot, Ideal.multiset_prod_eq_bot, ker_inr, LinearMap.not_hasEigenvalue_zero_tfae, Ideal.relNorm_bot, IsSemisimpleModule.jacobson_eq_bot, isIsotypic_iff_isFullyInvariant_imp_bot_or_top, dualAnnihilator_eq_bot_iff, bot_eq_top_of_rank_eq_zero, LieSubalgebra.bot_toSubmodule, Representation.invtSubmodule.coe_bot, LieSubmodule.toSubmodule_eq_bot, isSMulRegular_iff_ker_lsmul_eq_bot, pNilradical_eq_bot_of_frobenius_inj, LinearEquiv.ker, Valuation.leSubmodule_zero, Finsupp.ker_lsingle, dualAnnihilator_eq_bot_iff', LinearMap.ker_lsmul, Module.End.invtSubmodule.mk_eq_bot_iff, QuotientTorsion.torsion_eq_bot, Module.End.genEigenspace_zero, Polynomial.annIdealGenerator_eq_zero_iff, span_zero, LinearMap.ker_eq_bot_range_liftQ_iff, Ideal.bot_quotient_isMaximal_iff, Ideal.height_bot, LinearDisjoint.linearIndependent_left_of_flat, IsArtinianRing.isSemisimpleRing_iff_jacobson, LieAlgebra.IsKilling.ker_killingForm_eq_bot, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, LinearMap.ker_single, Ideal.bot_liesOver_bot, LinearMap.le_ker_iff_map, Module.End.invtSubmodule.bot_mem, Ideal.bot_prime, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, LinearMap.ker_eq_bot_of_inverse, Module.jacobson_quotient_jacobson, localized'_bot, HenselianRing.jac, Ideal.cotangentIdeal_square, eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator, isOrtho_bot_left, pNilradical_eq_bot', Ideal.mul_eq_bot, comap_bot, bot_colon, Module.Finite.iff_cofg_bot, LinearDisjoint.bot_left, annihilator_eq_top_iff, traceDual_top, Ring.jacobson_quotient_jacobson, colon_bot, eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator, eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator, toConvexCone_bot, bot_toAddSubgroup, Module.Basis.eval_ker, RingPreordering.support_eq_bot, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, UniformSpace.inseparableSetoid_ring, disjoint_iff_comap_eq_bot, linearIndepOn_iff_linearCombinationOn, ArchimedeanClass.closedBall_top, Ideal.map_eq_bot_iff_le_ker, Ideal.mem_jacobson_bot, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, FractionalIdeal.coe_zero, iSupIndep.subtype_ne_bot_le_finrank_aux, Representation.invtSubmodule.bot_mem, Ideal.eq_bot_of_liesOver_bot, mul_bot, spanRank_bot, Module.End.injOn_iInf_maxGenEigenspace, vectorSpan_of_subsingleton, IsDedekindDomain.flat_iff_torsion_eq_bot
|
instInfSet π | CompOp | 157 mathmath: LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, AlgebraicGeometry.Scheme.zeroLocus_iInf, Ideal.eq_jacobson_iff_sInf_maximal, span_sInf_le, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, LinearMap.ker_pi, Ideal.IsHomogeneous.sInf, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, DividedPowers.SubDPIdeal.sInf_carrier_def, DividedPowers.isSubDPIdeal_iInf, TruncatedWittVector.iInf_ker_truncate, Ideal.quotientInfToPiQuotient_inj, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, mem_iInf, HomogeneousIdeal.toIdeal_iInf, Ideal.quotientInfToPiQuotient_surj, Ideal.iInf_mul, inf_iInf, LinearMap.iInf_ker_proj, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, Ideal.sInf_isPrime_of_isChain, AlgebraicGeometry.Scheme.zeroLocus_biInf, Finsupp.iInf_ker_lapply_le_bot, Ideal.comap_iInf, LinearMap.iInf_ker_proj_le_iSup_range_single, LinearMap.ker_smul', annihilator_iSup, iInf_colon_iSup, Ideal.ker_Pi_Quotient_mk, LieSubmodule.sInf_toSubmodule, comap_iInf_map_of_injective, ContinuousLinearMap.iInf_ker_proj, Algebra.sInf_toSubmodule, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, Ideal.comap_sInf', Ideal.isRadical_iInf, Hausdorffification.instIsHausdorff, dualCoannihilator_iSup_eq, Ideal.eq_jacobson_iff_sInf_maximal', Pi.ker_ringHom, LinearMap.iSup_range_single_eq_iInf_ker_proj, isJacobsonRing_iff_sInf_maximal, IsHausdorff.iInf_pow_smul, Ideal.iInf_sup_eq_top, biInf_comap_proj, mem_set_smul_def, Ideal.iInf_span_singleton_natCast, LieSubalgebra.sInf_toSubmodule, iInf_coe, iSup_dualAnnihilator_le_iInf, comap_iInf, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, Ideal.Filtration.sInf_N, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, Ideal.Filtration.iInf_N, ClosedSubmodule.orthogonal_eq_inter, Finsupp.supported_iInter, Ideal.mem_sInf, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, LieSubmodule.iInf_toSubmodule, ClosedSubmodule.toSubmodule_iInf, Ideal.IsHomogeneous.iInf, HomogeneousIdeal.toIdeal_sInf, AffineSubspace.direction_iInf_of_mem, Module.End.disjoint_iInf_maxGenEigenspace, coe_iInf, map_iInf, Ideal.comap_sInf, Ideal.ker_tensorProductMk_quotient, RootPairing.iInf_ker_root'_eq, Ideal.iSup_iInf_eq_top_iff_pairwise, sInf_orthogonal, Ideal.iInf_span_singleton, pi_liftQ_eq_liftQ_pi, Ideal.radical_eq_sInf, RootPairing.iInf_ker_coroot'_eq, sInf_coe, AffineSubspace.direction_iInf, neg_iInf, Module.End.mem_iInf_maxGenEigenspace_iff, Algebra.iInf_toSubmodule, Ideal.instIsTwoSidedIInf, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, Subspace.dualAnnihilator_iInf_eq, Ideal.iInf_pow_eq_bot_of_isLocalRing, PointedCone.dual_iUnion, Ideal.mem_iInf, LieSubmodule.sInf_toSubmodule_eq_iInf, annihilator_span, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, Ideal.sup_iInf_eq_top, LinearMap.eventually_iInf_range_pow_eq, PrimeSpectrum.nilradical_eq_iInf, Ideal.mem_iInf_smul_pow_eq_bot_iff, Hausdorffification.lift_comp_of, Module.annihilator_pi, Ideal.map_sInf, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, AffineSubspace.direction_sInf, iInf_orthogonal, AffineSubspace.direction_iInf_of_mem_iInf, AffineSubspace.direction_sInf_of_mem, HomogeneousIdeal.toIdeal_iInfβ, map_iInf_comap_of_surjective, Ideal.radical_iInf_le, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', Ideal.iInf_pow_eq_bot_of_isDomain, mem_sInf, Ideal.isCoprime_biInf, Ideal.map_iInf_comap_of_surjective, Ideal.quotientInfToPiQuotient_mk', iInf_colon, Hausdorffification.lift_of, iInf_colon_iUnion, Ideal.quotientInfToPiQuotient_mk, Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq, nilradical_eq_sInf, inf_iInf_maxGenEigenspace_of_forall_mapsTo, CoFG.sInf, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, Module.annihilator_dfinsupp, Ideal.mul_iInf, LinearMap.iSup_range_single_le_iInf_ker_proj, iSup_torsionBySet_ideal_eq_torsionBySet_iInf, LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute, Ideal.sInf_minimalPrimes, restrictScalars_iInf, Finsupp.lsingle_range_le_ker_lapply, isJacobsonRing_iff_sInf_maximal', orthogonal_eq_inter, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, comap_smul', dualAnnihilator_iSup_eq, IsLocalization.ideal_eq_iInf_comap_map_away, Ideal.IsHomogeneous.radical_eq, PointedCone.dual_sUnion, colon_iUnion, span_biInter, AffineSubspace.direction_sInf_of_mem_sInf, NonUnitalAlgebra.sInf_toSubmodule, ClosedSubmodule.toSubmodule_sInf, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, iInf_comap_proj, restrictScalars_sInf, PrimeSpectrum.vanishingIdeal_iUnion, Ring.jacobson_eq_sInf_isMaximal, Ideal.IsHomogeneous.iInfβ, span_sInf, CoFG.sInf_of_finite, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, Ideal.comap_jacobson, coe_sInf, NonUnitalAlgebra.iInf_toSubmodule, Module.End.injOn_iInf_maxGenEigenspace
|
instMin π | CompOp | 150 mathmath: finrank_sup_add_finrank_inf_eq, prod_inf_prod, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, LinearMap.prod_eq_inf_comap, AffineSubspace.direction_inf, comap_inf, Ideal.mul_eq_inf_of_coprime, Ideal.comap_inf, isNoetherian_submodule_right, toConvexCone_inf, AffineSubspace.direction_inf_of_mem, LinearDisjoint.not_linearIndependent_pair_of_flat_left, DividedPowers.isSubDPIdeal_iInf, LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt, FractionalIdeal.coe_inf, IdealFilter.isTorsionQuot_inter_left_iff, inf_iInf, LinearPMap.sub_domain, PrimeSpectrum.union_zeroLocus, IsFractional.inf_right, map_comap_eq, finrank_add_inf_finrank_orthogonal, map_inf_comap_of_surjective, LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot, Finsupp.supported_inter, colon_union, PointedCone.dual_union, Ideal.Filtration.inf_N, Ideal.map_inf_comap_of_surjective, Subrepresentation.toSubmodule_inf, IsLocalization.map_inf, LinearDisjoint.not_linearIndependent_pair_of_flat_right, Ideal.IsPrime.inf_le, Ideal.inf_mul, localized'_inf, ProjectiveSpectrum.union_zeroLocus, inf_genEigenspace, LinearDisjoint.rank_inf_le_one_of_flat, Ideal.radical_inf, Ideal.IsPrimary.inf, LinearMap.comap_leq_ker_subToSupQuotient, FractionalIdeal.coeIdeal_inf, Ideal.IsRadical.inf, LinearMap.quotientInfEquivSupQuotient_apply_mk, Function.Exact.exact_mapQ_iff, Module.End.genEigenspace_inf_le_add, fst_inf_snd, map_inf_eq_map_inf_comap, PointedCone.dual_insert, IsLattice.inf, LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict, LinearPMap.sub_apply, smul_top_inf_eq_smul_of_isSMulRegular_on_quot, LinearMap.quotientInfEquivSupQuotient_injective, dualAnnihilator_sup_eq, AlgebraicGeometry.Scheme.zeroLocus_inf, dualCoannihilator_sup_eq, Ideal.Filtration.inf_submodule, finiteDimensional_inf_right, inf_iSup_genEigenspace, LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, mem_inf, comap_inf_map_of_injective, PrimeSpectrum.vanishingIdeal_union, Affine.Simplex.direction_mongePlane, LinearPMap.add_apply, Algebra.inf_toSubmodule, DividedPowers.SubDPIdeal.inf_carrier_def, LinearMap.IsSymmetric.directSum_isInternal_of_commute, Module.End.invtSubmodule.inf_mem, inf_orthogonal, Ideal.sup_mul_inf, coe_inf, Ideal.quotientInfEquivQuotientProd_snd, ContinuousLinearMap.ker_prod, sup_orthogonal_inf_of_hasOrthogonalProjection, sup_dualAnnihilator_le_inf, inf_comap_le_comap_add, DividedPowers.isSubDPIdeal_ker, Ideal.IsHomogeneous.inf, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, map_inf, eq_iSup_inf_genEigenspace, LinearDisjoint.not_linearIndependent_pair_of_flat, Ideal.mem_inf, RingFilterBasis.SubmodulesBasis.inter, finrank_add_inf_finrank_orthogonal', SubmodulesRingBasis.inter, span_singleton_inf_span_singleton, LinearMap.ker_prod, LinearMap.comap_prod_prod, NonUnitalAlgebra.inf_toSubmodule, LinearMap.span_singleton_inf_orthogonal_eq_bot, Ideal.map_inf_le, IsPrimary.inf, Ideal.mul_le_inf, map_strict_mono_or_ker_sup_lt_ker_sup, LinearMap.coe_quotientInfToSupQuotient, AffineSubspace.direction_inf_of_mem_inf, ClosedSubmodule.toSubmodule_inf, span_inter, LieSubalgebra.inf_toSubmodule, Ideal.radicalInfTopHom_apply, inf_orthogonal_eq_bot, Ideal.quotientInfEquivQuotientProd_fst, neg_inf, inf_iInf_maxGenEigenspace_of_forall_mapsTo, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, Ideal.lcm_eq_inf, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, isNoetherian_submodule_left, map_orthogonal, CoFG.inf, PrimeSpectrum.zeroLocus_inf, IdealFilter.IsTorsionQuot.inf, LinearMap.injective_domRestrict_iff, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal, LinearPMap.domRestrict_domain, DividedPowers.isSubDPIdeal_inf_iff, map_comap_subtype, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, Ideal.inf_eq_mul_of_isCoprime, Ideal.mul_inf, Ideal.fst_comp_quotientInfEquivQuotientProd, rank_sup_add_rank_inf_eq, LinearMap.BilinForm.finrank_add_finrank_orthogonal, inf_colon, ProjectiveSpectrum.zeroLocus_inf, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, Ideal.snd_comp_quotientInfEquivQuotientProd, SubmodulesBasis.inter, localizedβ_inf, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, Affine.Simplex.direction_altitude, HomogeneousIdeal.toIdeal_inf, Subspace.dualAnnihilator_inf_eq, LinearPMap.add_domain, LinearDisjoint.rank_inf_le_one_of_flat_right, LinearMap.quotientInfEquivSupQuotient_surjective, LinearDisjoint.rank_inf_le_one_of_flat_left, inf_coe, map_inf_le, finiteDimensional_inf_left, Ideal.radical_mul, LieSubmodule.inf_toSubmodule, Ideal.exists_pow_inf_eq_pow_smul, restrictScalars_inf, colon_inf_eq_left_of_subset, Module.annihilator_prod, comap_subtype_le_iff
|
instOrderBot π | CompOp | 63 mathmath: disjoint_span_singleton', Module.End.isSemisimple_restrict_iff, supIndep_torsionBySet_ideal, Polynomial.disjoint_ker_aeval_of_isCoprime, LinearMap.injective_restrict_iff_disjoint, Ideal.sum_eq_sup, orthogonal_disjoint, Module.End.invtSubmodule.disjoint_mk_iff, IsSimpleRing.tfae, LieSubmodule.disjoint_toSubmodule, linearIndepOn_id_union_iff, isSimpleModule_iff_isAtom, RootPairing.disjoint_corootSpan_ker_corootForm, LinearMap.disjoint_inl_inr, LinearIndependent.disjoint_span_image, RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule, finiteDimensional_finset_sup, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint, linearIndependent_sum, disjoint_span_singleton, IsSimpleModule.isAtom, HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum, LinearMap.disjoint_ker, atom_iff_nonzero_span, TensorAlgebra.ΞΉ_range_disjoint_one, ExteriorAlgebra.ΞΉ_range_disjoint_one, nonzero_span_atom, linearIndepOn_iff_disjoint, disjoint_ker_of_finrank_le, Module.End.disjoint_genEigenspace, LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker, Module.End.isFinitelySemisimple_iff, fg_finset_sup, Module.End.disjoint_iInf_maxGenEigenspace, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, Finsupp.disjoint_supported_supported, disjoint_def', Module.End.eventually_disjoint_ker_pow_range_pow, linearIndepOn_union_iff, supIndep_torsionBy, LinearMap.disjoint_ker_iff_injOn, disjoint_span_singleton_of_notMem, isCompl_iff_disjoint, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Finsupp.disjoint_lsingle_lsingle, LinearMap.disjoint_ker_of_nondegenerate_restrict, IsOrtho.disjoint, ModuleCat.disjoint_span_sum, finite_finset_sup, Module.End.generalized_eigenvec_disjoint_range_ker, LinearMap.disjoint_single_single, disjoint_def, range_ker_disjoint, instIsAtomisticSubmodule, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, RootPairing.disjoint_rootSpan_ker_rootForm, LinearMap.disjoint_ker', NumberField.mixedEmbedding.disjoint_span_commMap_ker, Finsupp.disjoint_supported_supported_iff, Finsupp.lmapDomain_disjoint_ker, Module.End.invtSubmodule.disjoint_iff, disjoint_iff_comap_eq_bot, disjoint_span_singleton''
|
instOrderTop π | CompOp | 40 mathmath: codisjoint_span_image_of_codisjoint, Ideal.comap_finsetInf, colon_finsetInf, Ideal.isPrimary_finsetInf, Ideal.prod_le_inf, mem_finset_inf, Ideal.IsPrime.inf_le', Ideal.isPrimary_finset_inf, codisjoint_iff_exists_add_eq, IsMinimalPrimaryDecomposition.inf_eq, Finsupp.codisjoint_supported_supported, isCoatom_comap_iff, RingOfIntegers.not_dvd_exponent_iff, comap_finsetInf, coe_finsetInf, Ideal.finset_inf_span_singleton, Ideal.isCoprime_tfae, IsMinimalPrimaryDecomposition.minimal, Module.Finite.instIsCoatomicSubmodule, IsDedekindDomain.inf_prime_pow_eq_prod, Ideal.IsMaximal.out, Finsupp.codisjoint_supported_supported_iff, IsSemisimpleModule.isCoatomic_submodule, Module.End.invtSubmodule.codisjoint_iff, LinearMap.isCoatom_ker_of_surjective, LieSubmodule.codisjoint_toSubmodule, Ideal.eq_inf_of_isPrime_inf, isSimpleModule_iff_isCoatom, finset_inf_coe, LinearMap.eventually_codisjoint_ker_pow_range_pow, mem_finsetInf, Ideal.multiset_prod_le_inf, Ideal.radical_finset_inf, Ideal.isCoprime_iff_codisjoint, Module.End.invtSubmodule.codisjoint_mk_iff, isPrimary_finsetInf, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Ideal.instIsCoatomic, IsCoprime.codisjoint, Ideal.isMaximal_def
|
instTop π | CompOp | 592 mathmath: Ideal.isPrime_ideal_prod_top, FractionalIdeal.coeIdeal_top, Ideal.maximal_of_no_maximal, colon_empty, topEquiv_symm_apply_coe, AdicCompletion.val_sub_apply, LieSubalgebra.top_toSubmodule, LinearPMap.zero_domain, comap_zero, Ideal.eq_jacobson_iff_sInf_maximal, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, LinearMap.eqLocus_same, Module.support_quotient, range_snd, top_mul_eq_top_of_mul_eq_one, AdicCompletion.AdicCauchySequence.mk_eq_mk, LinearMap.range_id, LinearMap.ker_eq_top, Ideal.map_eq_top_iff_of_ker_le, RingTheory.Sequence.isWeaklyRegular_cons_iff', Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, isInternal_prime_power_torsion_of_pid, AdicCompletion.map_val_apply, top_toAddSubmonoid, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, RingHom.ker_eq_top_of_subsingleton, Ideal.smul_top_eq_map, localizedβ_top, RingTheory.Sequence.isWeaklyRegular_cons_iff, Module.Relations.Solution.surjective_Ο_iff_span_eq_top, Module.isTorsionBySet_quotient_set_smul, span_fourier_closure_eq_top, Polynomial.Sequence.span, Module.Finite.fg_top, dense_iff_topologicalClosure_eq_top, span_setOf_mem_eq_top, LinearMap.range_eq_top_of_surjective, Ideal.one_eq_top, closedComplemented_top, Profinite.NobelingProof.Products.span_nil_eq_top, Ideal.under_top, Ideal.height_top, Ideal.natCast_eq_top, Polynomial.contentIdeal_one, TensorProduct.span_tmul_eq_top, fst_sup_snd, Module.isTorsionBySet_quotient_ideal_smul, QuotSMulTop.equivTensorQuot_naturality, top_eq_ofList_cons_smul_iff, unique_quotient_iff_eq_top, AdicCompletion.val_smul, RootPairing.span_orbit_eq_top, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, AdicCompletion.incl_apply, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, AdicCompletion.val_smul_eq_evalβ_smul, eq_top_iff', PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal, Module.supportDim_add_length_eq_supportDim_of_isRegular, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, LinearMap.isUnit_iff_range_eq_top, CStarAlgebra.span_nonneg_inter_unitBall, Module.Basis.flag_last, Ideal.minimalPrimes_top, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, isotypicComponent_eq_top_iff, neg_top, Module.jacobson_lt_top, Ideal.ideal_prod_prime, LinearMap.iSup_range_single, AffineSubspace.direction_eq_top_iff_of_nonempty, RootPairing.span_coroot'_eq_top, comap_fst, Ideal.map_eq_top_or_isMaximal_of_surjective, Ideal.Quotient.subsingleton_iff, RingTheory.Sequence.isRegular_cons_iff, QuotSMulTop.equivTensorQuot_naturality_mk, restrictScalars_top, dualAnnihilator_eq_top_iff, orthogonal_eq_bot_iff, Ring.jacobson_smul_top_le, AffineSubspace.linear_topEquiv, isFiniteLength_iff_exists_compositionSeries, pow_smul_top_le, groupHomology.cyclesβ_eq_top_of_isTrivial, biSup_comap_subtype_eq_top, QuotSMulTop.map_comp_mkQ, LinearMap.range_domRestrict_eq_range_iff, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, Ideal.relNorm_top, LinearMap.span_singleton_sup_orthogonal_eq_top, span_range_inclusion_restrictScalars_eq_top, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, ImplicitFunctionData.range_leftDeriv, ExteriorAlgebra.ΞΉMulti_span, Ideal.isIdempotentElem_iff_eq_bot_or_top, Ideal.sup_eq_top_iff_isCoprime, AdicCompletion.pi_apply_coe, Ideal.isPrime_ideal_prod_top', RingTheory.Sequence.isWeaklyRegular_iff_Fin, span_singleton_eq_top_iff, PrimeSpectrum.iSup_basicOpen_eq_top_iff, AdicCompletion.val_add_apply, AdicCompletion.smul_eval, ModuleCat.smulShortComplex_Xβ_isAddCommGroup, Ideal.toCotangent_range, RootPairing.IsIrreducible.eq_top_of_invtSubmodule_coreflection, rank_le_spanRank, Ideal.adic_module_basis, Polynomial.isPrimitive_iff_contentIdeal_eq_top, Finsupp.supported_univ, Ideal.jacobson_eq_top_iff, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, topEquiv_apply, KaehlerDifferential.span_range_map_derivation_of_isLocalization, sSup_isotypicComponents, Profinite.NobelingProof.GoodProducts.spanFin, map_top, range_mkQ, spanRank_range_le, QuotSMulTop.map_surjective, toConvexCone_top, localized'_top, LinearIndependent.span_eq_top_of_card_eq_finrank', Ideal.eq_bot_or_top, eq_top_of_nonempty_interior', LieSubmodule.mk_eq_top_iff, CStarAlgebra.span_nonneg, Representation.invtSubmodule.coe_top, Hausdorffification.instIsHausdorff, traceDual_top', PrimeSpectrum.vanishingIdeal_eq_top_iff, AdicCompletion.mkβ_apply_coe, Ideal.span_singleton_one, torsionBy_torsionBy_eq_top, Ideal.span_eq_top_iff_finite, Ideal.eq_top_of_isUnit_mem, Ideal.span_single_eq_top, Ideal.Quotient.span_singleton_one, starProjection_top', AdicCompletion.isAdicCauchy_iff, LinearMap.BilinForm.orthogonal_eq_bot_iff, IsCoercive.range_eq_top, LinearMap.range_eq_top_of_cancel, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, IsLocalRing.map_tensorProduct_mk_eq_top, AdicCompletion.val_sum, Ideal.eq_jacobson_iff_sInf_maximal', Ideal.comap_eq_top_iff, LinearMap.range_rangeRestrict, isJacobsonRing_iff_sInf_maximal, Ideal.FiniteHeight.eq_top_or_height_ne_top, torsion_torsion_eq_top, Convex.span_tangentConeAt, IsHausdorff.iInf_pow_smul, Module.isTorsionBySet_iff_torsionBySet_eq_top, LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank, Module.length_top, SymmetricPower.span_tprod_eq_top, span_range_inclusion_eq_top, prod_top, map_mkQ_eq_top, eq_top_of_disjoint, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, map_eq_top_iff, Algebra.top_toSubmodule, isTorsion'_iff_torsion'_eq_top, Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one, KaehlerDifferential.span_range_derivation, ModuleCat.range_eq_top_of_epi, AdicCompletion.range_eval, Ideal.Quotient.smul_top, AdicCompletion.val_neg_apply, CStarAlgebra.span_nonneg_inter_unitClosedBall, Ideal.eq_bot_of_minimalPrimes_eq_empty, Module.Quotient.mk_smul_mk, top_toAddSubgroup, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime, top_isPrincipal, Ideal.Filtration.top_N, MvPolynomial.restrictSupport_univ, PointedCone.dual_empty, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, DFinsupp.iSup_range_lsingle, AdicCompletion.transitionMap_comp_eval, ModuleCat.smulShortComplex_g, isOrtho_top_left, Polynomial.sup_aeval_range_eq_top_of_isCoprime, MvPolynomial.map_restrict_dom_evalβ, subsingleton_quotient_iff_eq_top, snd_map_snd, LieSubmodule.top_toSubmodule, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, exists_compositionSeries_of_isNoetherian_isArtinian, jacobson_smul_lt_top, dualCoannihilator_bot, pi_empty, AdicCompletion.coe_eval, RootPairing.invtRootSubmodule.top_mem, dualCoannihilator_top, AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, LinearMap.sup_range_inl_inr, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, IsLocalizedModule.subsingleton_iff_ker_eq_top, comap_subtype_self, RieszExtension.exists_top, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, LinearMap.span_singleton_sup_ker_eq_top, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, LinearMap.IsPerfectCompl.left_top_iff, Module.Basis.eval_range, AdicCompletion.val_mul, annihilator_bot, RootPairing.isIrreducible_iff, RootPairing.GeckConstruction.span_range_h'_eq_top, span_univ, smul_top_inf_eq_smul_of_isSMulRegular_on_quot, ConvexCone.toPointedCone_top, AdicCompletion.mk_smul_mk, top_colon, LocalizedModule.subsingleton_iff_ker_eq_top, Ideal.span_singleton_eq_top, Module.FaithfullyFlat.iff_flat_and_ideal_smul_eq_top, LocalSubring.map_maximalIdeal_eq_top_of_isMax, span_range_eq_top_iff_surjective_fintypeLinearCombination, isCoatom_comap_or_eq_top, top_orthogonal_eq_bot, HilbertBasis.dense_span, Ideal.finiteHeight_iff, Module.Basis.toDual_range, isSimpleRing_iff_isTwoSided_imp, LinearMap.IsPerfectCompl.right_top_iff, ConvexCone.IsGenerating.top_le_span, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, Module.annihilator_eq_top_iff, pi_top, QuotSMulTop.equivQuotTensor_naturality, Finsupp.linearCombinationOn_range, HomogeneousLocalization.Away.span_mk_prod_pow_eq_top, AdicCompletion.transitionMap_comp_reduceModIdeal, FractionalIdeal.coe_one_eq_coeSubmodule_top, Ideal.torsionOf_zero, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, comap_snd, Ideal.ofNat_eq_top, LinearMap.exact_smul_id_smul_top_mkQ, IsSemisimpleModule.finite_tfae, FractionalIdeal.coe_inv_of_ne_zero, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, comap_subtype_eq_top, AffineSubspace.mk'_top, Profinite.NobelingProof.GoodProducts.span, Matrix.range_toLin_eq_top, AdicCompletion.smul_mk, Ideal.matrix_top, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, LinearMap.IsProj.top, RootPairing.IsRootSystem.span_root_eq_top, annihilator_top_inter_nonZeroDivisors, Ideal.fg_top, prod_eq_top_iff, RingTheory.Sequence.isWeaklyRegular_append_iff', RootPairing.isSimpleModule_weylGroupRootRep_iff, IsCoprime.sup_eq, LinearMap.range_eq_top, Ideal.ker_tensorProductMk_quotient, PointedCone.dual_zero, Ideal.span_one, span_selfAdjoint, colon_eq_top_iff_subset, ZSpan.span_top, IsLattice.span_eq_top, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, Subspace.exists_eq_top_of_iUnion_eq_univ, Ideal.iSup_iInf_eq_top_iff_pairwise, colon_singleton_zero, Ideal.isCoprime_tfae, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, rank_eq_spanRank_of_free, Module.End.invtSubmodule.mk_eq_top_iff, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, QuotSMulTop.map_exact, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, RingTheory.Sequence.isWeaklyRegular_append_iff, IsArtinian.disjoint_partial_infs_eventually_top, Module.supportDim_quotSMulTop_succ_eq_supportDim, PrimeSpectrum.vanishingIdeal_empty, SymmetricPower.range_mk, Ideal.prod_eq_top_iff, HomogeneousIdeal.toIdeal_top, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, torsionBySet_torsionBySet_eq_top, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_top_iff, Ideal.top_liesOver_top, span_lt_top_of_card_lt_finrank, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, Ideal.map_eq_top_iff, biSup_comap_eq_top_of_range_eq_biSup, Module.Relations.Solution.isPresentation_iff, IsPrecomplete.top, Ideal.toCotangent_apply, Ideal.eq_top_iff_one, IsSemisimpleModule.sSup_simples_eq_top, Ideal.absNorm_top, Finsupp.linearCombination_range, LinearIndependent.span_eq_top_of_card_eq_finrank, top_le_span_range_iff_forall_exists_fun, Ideal.eq_top_of_unit_mem, isOrtho_top_right, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, fst_map_fst, Profinite.NobelingProof.spanFinBasis.span, RootPairing.span_root'_eq_top, Ideal.adic_basis, AffineSubspace.direction_top, Module.finite_def, finrank_top, LinearIndependent.repr_range, TensorProduct.mapβ_mk_top_top_eq_top, Module.isTorsionBySet_annihilator_top, TensorProduct.quotTensorEquivQuotSMul_symm_mk, LinearMap.range_le_iff_comap, cardQuot_eq_one_iff, Module.Baer.extensionOfMax_to_submodule_eq_top, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, AdicCompletion.val_add, Absorbent.submodule_eq_top, Ideal.not_isPrime_iff, Module.supportDim_le_supportDim_quotSMulTop_succ, QuotSMulTop.equivQuotTensor_naturality_mk, Module.exists_isPrincipal_quotient_of_finite, span_fourierLp_closure_eq_top, Algebra.toSubmodule_eq_top, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, TwoSidedIdeal.top_asIdeal, AdicCompletion.val_one, WithCStarModule.map_top_submodule, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, mem_smul_top_iff, Module.support_quotSMulTop, ContinuousMap.setOfTop_eq_univ, ImplicitFunctionData.range_rightDeriv, CStarAlgebra.span_nonneg_inter_closedBall, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, LinearMap.ker_zero, Ideal.isCompactElement_top, IsZLattice.span_top, Ideal.mem_iInf_smul_pow_eq_bot_iff, Hausdorffification.lift_comp_of, NonUnitalAlgebra.toSubmodule_eq_top, topologicalClosure_eq_top_iff, Module.FinitePresentation.out, FractionalIdeal.coe_inv_of_nonzero, MvPolynomial.vanishingIdeal_empty, Ideal.torsionOf_eq_top_iff, IsLocalRing.span_eq_top_of_tmul_eq_basis, sup_orthogonal_of_hasOrthogonalProjection, PreTilt.exists_smodEq_untiltAux, Ideal.absNorm_eq_one_iff, AdicCompletion.transitionMap_map_pow, eq_top_iff_forall_basis_mem, Representation.invtSubmodule.top_mem, IsAssociatedPrime.annihilator_le, starProjection_top, Ideal.instIsTwoSidedTop, submoduleOf_eq_top, Module.rank_le_one_iff_top_isPrincipal, dualAnnihilator_top, ConvexCone.IsGenerating.span_eq_top, ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, AdicCompletion.val_sub, IsHausdorff.eq_iff_smodEq, IsSimpleModule.span_singleton_eq_top, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, Module.Finite.top, Ideal.IsMaximal.coprime_of_ne, Ideal.top_mul, Module.End.invtSubmodule.top_mem, AdicCompletion.val_neg, Ideal.isUnit_iff, LieSubalgebra.toSubmodule_eq_top, IsLocalRing.CotangentSpace.map_eq_top_iff, LinearMap.BilinForm.orthogonal_top_eq_ker, isInternal_prime_power_torsion, annihilator_top, AdicCompletion.transitionMap_ideal_mk, sup_eq_top_iff, traceDual_bot, AdicCompletion.transitionMap_map_mul, fg_top, Profinite.NobelingProof.GoodProducts.span_iff_products, Subspace.top_mem_of_biUnion_eq_univ, LinearMap.eqLocus_eq_top, LinearMap.IsProj.submodule_eq_top_iff, CliffordAlgebra.iSup_ΞΉ_range_eq_top, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, span_flip_eq_top_iff_linearIndependent, CoFG.top, LieModule.maxGenEigenSpace_toEnd_eq_top, Ideal.jacobson_top, Ideal.sup_height_eq_ringKrullDim, toAddSubgroup_eq_top, Ideal.IsHomogeneous.top, Ideal.radicalInfTopHom_apply, Hausdorffification.lift_of, orthogonal_eq_top_iff, map_subtype_top, LinearMap.BilinForm.orthogonal_bot, QuotSMulTop.map_comp, LieSubmodule.iSup_toSubmodule_eq_top, Ideal.finiteHeight_iff_lt, span_span_coe_preimage, mul_top_eq_top_of_mul_eq_one, span_range_eq_top_iff_surjective_finsuppLinearCombination, SModEq.top, subalgebra_top_finrank_eq_submodule_top_finrank, IsLocalRing.CotangentSpace.span_image_eq_top_iff, isPrecomplete_iff, MvPolynomial.zeroLocus_top, RootPairing.coe_top, Ideal.eq_top_of_norm_lt_one, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, Module.AEval.annihilator_top_eq_ker_aeval, Ideal.eq_prime_pow_mul_coprime, Ideal.radical_top, LinearMap.range_eq_map, UnitAddTorus.span_mFourier_closure_eq_top, Ideal.comap_top, Ideal.prod_top_top, DirectSum.IsInternal.submodule_iSup_eq_top, Ideal.map_top, top_smul, Ideal.eq_top_iff_of_liesOver, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, Ideal.minimalPrimes_eq_empty_iff, span_eq_top_of_ne_zero, Module.length_eq_height, bot_orthogonal_eq_top, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, conductor_eq_top_iff_adjoin_eq_top, LinearMap.ker_eq_bot_iff_range_eq_top, QuotSMulTop.map_apply_mk, dualAnnihilator_bot, AdicCompletion.eval_of, Ideal.span_univ, map_range_rTensor_subtype_lid, LinearMap.BilinForm.orthogonal_eq_top_iff, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal, IsLocalization.span_invSubmonoid, top_coe, RootPairing.span_root_image_eq_top_of_forall_orthogonal, linearProjOfIsCompl_range, PiTensorProduct.span_tprod_eq_top, finrank_eq_one_iff_of_nonzero, PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal, Module.End.iSup_maxGenEigenspace_eq_top, Quotient.subsingleton_iff, conductor_eq_top_of_powerBasis, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, cardQuot_top, restrictScalars_eq_top_iff, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, Ideal.ideal_prod_prime_aux, LinearMap.BilinForm.orthogonal_top_eq_bot, span_range_subtype_eq_top_iff, spanRank_top, Ideal.top_pow, ClosedSubmodule.toSubmodule_top, baseChange_top, Module.Flat.top_mul_submoduleAlgebra, AdicCompletion.val_zero, isJacobsonRing_iff_sInf_maximal', sSup_simples_eq_top_iff_isSemisimpleModule, Ideal.mul_top, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, Ideal.pow_eq_top_iff, AdicCompletion.mk_apply_coe, isNoetherian_top_iff, DualNumber.ideal_trichotomy, IsLocalRing.map_mkQ_eq_top, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, LieSubmodule.toSubmodule_eq_top, Ideal.radical_eq_top, RootPairing.rootSpan_eq_top_iff, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, mk_eq_top, CStarAlgebra.span_nonneg_inter_ball, RingTheory.Sequence.isWeaklyRegular_iff, LinearMap.range_eq_of_proj, Module.Basis.span_eq, instHasOrthogonalProjectionTop, LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot, AdicCompletion.transitionMap_comp_eval_apply, ModuleCat.smulShortComplex_Xβ_isModule, Module.surjective_piEquiv_apply_iff, isIsotypic_iff_isFullyInvariant_imp_bot_or_top, span_range_eq_top_of_injective_of_rank_le, dualAnnihilator_eq_bot_iff, TensorProduct.quotTensorEquivQuotSMul_comp_mk, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, rank_top, bot_eq_top_of_rank_eq_zero, LieAlgebra.IsKilling.span_weight_eq_top, IsLocalFrameOn.generating, AdicCompletion.val_zero_apply, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, LinearMap.BilinForm.finrank_add_finrank_orthogonal, HomogeneousIdeal.eq_top_iff, NonUnitalAlgebra.top_toSubmodule, RootPairing.EmbeddedG2.span_eq_top, HahnEmbedding.Partial.exists_domain_eq_top, QuotSMulTop.map_id, PrimeSpectrum.zeroLocus_empty_iff_eq_top, Module.isPrincipal_def, RootPairing.IsRootSystem.span_coroot_eq_top, smul_top_le_comap_smul_top, set_smul_top_eq_span, Ideal.isCoprime_iff_sup_eq, PrimeSpectrum.iSup_basicOpen_eq_top_iff', AdicCompletion.eval_surjective, Module.Basis.mk_eq_spanRank, exteriorPower.ΞΉMulti_span, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, IsLocalization.coeSubmodule_top, Ideal.eq_top_of_mk_tensor_eq_one, conductor_eq_top_of_adjoin_eq_top, spanRank_eq_of_equiv, Module.Finite.exists_fin, torsion'_torsion'_eq_top, UnitAddTorus.span_mFourierLp_closure_eq_top, RootPairing.eq_top_of_mem_invtSubmodule_of_forall_eq_univ, mem_top, ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz, AdicCompletion.transitionMap_map_one, ModuleCat.epi_iff_range_eq_top, Ideal.spanNorm_top, LinearMap.ker_tensorProductMk, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, Module.isTorsionBy_iff_torsionBy_eq_top, Representation.invariants_eq_top, comap_top, coe_eq_univ, AdicCompletion.eval_apply, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, annihilator_eq_top_iff, Ring.jacobson_lt_top, RCLike.span_one_I, traceDual_top, RingTheory.Sequence.isRegular_cons_iff', colon_bot, Module.Basis.is_basis_iff_det, Ideal.Quotient.zero_eq_one_iff, IsPrincipal.isPrimitive_iff_contentIdeal_eq_top, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, Algebra.Extension.Cotangent.ker_mk, AdicCompletion.val_sum_apply, RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection, CStarAlgebra.span_unitary, AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top, Module.erange_coe, MvPolynomial.range_evalα΅’, submoduleOf_self, lt_top_of_finrank_lt_finrank, Finsupp.range_restrictDom, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, AdicCompletion.of_apply, Module.isTorsionBy_quotient_element_smul, LinearEquiv.range, Ideal.IsOka.top, range_fst, Ideal.exists_pow_inf_eq_pow_smul, subalgebra_top_rank_eq_submodule_top_rank, AdicCompletion.eval_comp_of, AdicCompletion.val_smul_apply, Module.Dual.range_eq_top_of_ne_zero, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, span_range_inclusionSpan, LinearMap.surjective_domRestrict_iff, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, map_le_smul_top, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, Finsupp.iSup_lsingle_range, Module.finrank_le_one_iff_top_isPrincipal, LinearMap.range_lt_top_of_det_eq_zero, eq_top_of_finrank_eq, LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top, HilbertBasis.finite_spans_dense
|
instUniqueOfSubsingleton π | CompOp | β |
topEquiv π | CompOp | 3 mathmath: topEquiv_symm_apply_coe, AffineSubspace.linear_topEquiv, topEquiv_apply
|
unique' π | CompOp | β |
uniqueBot π | CompOp | 1 mathmath: basisOfPid_bot
|