Submodule

📁 Source: Mathlib/RingTheory/Localization/Submodule.lean

Statistics

Metric	Count
Definitions coeSubmodule, Submodule	2
Theorems isNoetherianRing, coeSubmodule_injective, coeSubmodule_isPrincipal, coeSubmodule_le_coeSubmodule, coeSubmodule_strictMono, coeSubmodule_bot, coeSubmodule_fg, coeSubmodule_injective, coeSubmodule_isPrincipal, coeSubmodule_le_coeSubmodule, coeSubmodule_mono, coeSubmodule_mul, coeSubmodule_span, coeSubmodule_span_singleton, coeSubmodule_strictMono, coeSubmodule_sup, coeSubmodule_top, instIsNoetherianRingLocalization, isNoetherianRing, mem_coeSubmodule, mem_span_iff, mem_span_map	22
Total	24

Algebra.EssFiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNoetherianRing 📖	mathematical	—	IsNoetherianRing CommSemiring.toSemiring CommRing.toCommSemiring	—	IsLocalization.isNoetherianRing isLocalization Algebra.FiniteType.isNoetherianRing Algebra.instFiniteTypeSubtypeMemSubalgebraSubalgebra

IsFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeSubmodule_injective 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IsLocalization.coeSubmodule	—	Function.Injective.of_eq_imp_le coeSubmodule_le_coeSubmodule Eq.le
coeSubmodule_isPrincipal 📖	mathematical	—	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IsLocalization.coeSubmodule Semiring.toModule	—	IsLocalization.coeSubmodule_isPrincipal le_rfl
coeSubmodule_le_coeSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder IsLocalization.coeSubmodule Ideal Semiring.toModule	—	IsLocalization.coeSubmodule_le_coeSubmodule le_rfl
coeSubmodule_strictMono 📖	mathematical	—	StrictMono Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule PartialOrder.toPreorder Submodule.instPartialOrder Semiring.toModule IsLocalization.coeSubmodule	—	strictMono_of_le_iff_le coeSubmodule_le_coeSubmodule

IsLocalization

Definitions

Name	Category	Theorems
coeSubmodule 📖	CompOp	24 math math: coeSubmodule_mul, IsFractionRing.coeSubmodule_strictMono, coeSubmodule_span, FractionalIdeal.coe_coeIdeal, FractionalIdeal.mem_coeSubmodule, coeSubmodule_differentIdeal, coeSubmodule_differentIdeal_fractionRing, coeSubmodule_mono, coeSubmodule_bot, FractionalIdeal.coe_one_eq_coeSubmodule_top, FractionalIdeal.coe_inv_of_ne_zero, coeSubmodule_le_coeSubmodule, IsFractionRing.coeSubmodule_le_coeSubmodule, mem_coeSubmodule_conductor, coeSubmodule_strictMono, IsFractionRing.coeSubmodule_isPrincipal, mem_coeSubmodule, IsFractionRing.coeSubmodule_injective, coeSubmodule_fg, coeSubmodule_isPrincipal, coeSubmodule_top, coeSubmodule_sup, coeSubmodule_injective, coeSubmodule_span_singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeSubmodule_bot 📖	mathematical	—	coeSubmodule Bot.bot Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule Algebra.toModule	—	coeSubmodule.eq_1 Submodule.map_bot
coeSubmodule_fg 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Submodule.FG CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule coeSubmodule Semiring.toModule	—	Submodule.fg_of_fg_map_injective Submodule.FG.map
coeSubmodule_injective 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule coeSubmodule	—	Function.Injective.of_eq_imp_le coeSubmodule_le_coeSubmodule Eq.le
coeSubmodule_isPrincipal 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule coeSubmodule Semiring.toModule	—	Submodule.mem_span_singleton_self mem_coeSubmodule coeSubmodule_injective Ideal.submodule_span_eq coeSubmodule_span_singleton
coeSubmodule_le_coeSubmodule 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder coeSubmodule Ideal Semiring.toModule	—	Submodule.map_le_map_iff_of_injective RingHomSurjective.ids injective
coeSubmodule_mono 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder coeSubmodule	—	Submodule.map_mono
coeSubmodule_mul 📖	mathematical	—	coeSubmodule Ideal CommSemiring.toSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	Submodule.map_mul
coeSubmodule_span 📖	mathematical	—	coeSubmodule Ideal.span CommSemiring.toSemiring Submodule.span NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Set.image DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	coeSubmodule.eq_1 Ideal.span.eq_1 Submodule.map_span
coeSubmodule_span_singleton 📖	mathematical	—	coeSubmodule Ideal.span CommSemiring.toSemiring Set Set.instSingletonSet Submodule.span NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	coeSubmodule_span Set.image_singleton
coeSubmodule_strictMono 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	StrictMono Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule PartialOrder.toPreorder Submodule.instPartialOrder Semiring.toModule coeSubmodule	—	strictMono_of_le_iff_le coeSubmodule_le_coeSubmodule
coeSubmodule_sup 📖	mathematical	—	coeSubmodule Ideal CommSemiring.toSemiring SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	Submodule.map_sup
coeSubmodule_top 📖	mathematical	—	coeSubmodule Top.top Ideal CommSemiring.toSemiring Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule Algebra.toModule Submodule.one	—	coeSubmodule.eq_1 Submodule.map_top RingHomSurjective.ids Submodule.one_eq_range
instIsNoetherianRingLocalization 📖	mathematical	—	IsNoetherianRing Localization CommRing.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm	—	isNoetherianRing Localization.isLocalization
isNoetherianRing 📖	mathematical	—	IsNoetherianRing CommSemiring.toSemiring	—	isNoetherianRing_iff isNoetherian_iff OrderEmbedding.wellFounded
mem_coeSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership Submodule.setLike coeSubmodule Ideal Semiring.toModule DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	—
mem_span_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.span Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction mk' AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submodule.span_induction Submodule.subset_span mk'_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul Submodule.zero_mem Submodule.add_mem Submodule.smul_mem smul_add IsScalarTower.algebraMap_smul smul_smul mul_one mk'_mul mul_assoc mk'_spec mul_right_comm one_mul exists_mk'_eq mul_comm mul_mk'_eq_mk'_of_mul Submodule.span_subset_span
mem_span_map 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set.image DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike mk'	—	mem_span_iff IsScalarTower.right coeSubmodule_span Algebra.linearMap_apply smul_eq_mul mul_comm mul_mk'_eq_mk'_of_mul mul_one Submodule.map_mem_span_algebraMap_image IsScalarTower.left

(root)

Definitions

Name	Category	Theorems
Submodule 📖	CompData	4797 math math: DirectSum.IsInternal.ofBijective_coeLinearMap_same, Submodule.comap_lt_comap_iff_of_surjective, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Submodule.exists_lieSubmodule_coe_eq_iff, isArtinian_iff, TensorProduct.mapInclIsometry_apply, Submodule.coe_sum, ZLattice.summable_norm_zpow, Submodule.finrank_sup_add_finrank_inf_eq, Ideal.toCotangent_to_quotient_square, LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, TopModuleCat.hom_cokerπ, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, groupCohomology.instEpiModuleCatH2π, HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, Submodule.toAddSubgroup_toZModSubmodule, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, SModEq.bot, groupHomology.π_comp_H2Iso_hom_assoc, Submodule.toAddSubmonoid_toNatSubmodule, Submodule.prod_inf_prod, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, LinearMap.eqOn_span', Affine.Simplex.altitudeFoot_restrict, TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, Submodule.comap_le_comap_iff_of_le_range, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, Submodule.rTensorOne_symm_apply, AddMonoidAlgebra.supportedEquivFinsupp_apply_apply, iSupIndep.linearEquiv_symm_apply, lTensor.inverse_comp_lTensor, LinearMap.IsProj.map_mem, isNoetherian_iff', Submodule.mem_colon_span_singleton, LinearMap.prod_eq_inf_comap, AffineSubspace.direction_inf, Submodule.mul_one, Submodule.topEquiv_symm_apply_coe, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, AdicCompletion.val_sub_apply, Ideal.Filtration.submodule_closure_single, iSupIndep.dfinsupp_lsum_injective, LinearMap.BilinForm.dualSubmoduleParing_spec, Submodule.FG.rTensor.directedSystem, AffineSubspace.coe_vsub, AffineSubspace.direction_sup_eq_sup_direction, Submodule.quotientRel_def, Submodule.disjoint_span_singleton', Algebra.idealMap_eq_ofEq_comp_toLocalized₀, LinearMap.IsIdempotentElem.comp_eq_right_iff, Module.length_compositionSeries, Submodule.Quotient.eq, Module.End.pow_apply_mem_of_forall_mem, LieSubalgebra.top_toSubmodule, continuousOn_stereoToFun, Submodule.coe_continuous_linearProjOfClosedCompl', Submodule.QuotientBot.infinite, LinearMap.ker_le_of_iterateMapComap_eq_succ, groupHomology.mapCycles₂_comp_assoc, Module.End.isSemisimple_restrict_iff, FiniteArchimedeanClass.ball_lt_closedBall, isFullyInvariant_iff_sSup_isotypicComponents, Submodule.pow_zero, ContinuousLinearMap.IsIdempotentElem.isClosed_range, RootPairing.posRootForm_posForm_apply_apply, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, Module.Basis.mem_submodule_iff, LinearMap.BilinForm.dualSubmoduleToDual_apply_apply, Submodule.coe_add, LinearPMap.zero_domain, Submodule.supIndep_torsionBySet_ideal, LinearMap.iterateRange_succ, OrthonormalBasis.orthogonalProjection_eq_sum, Submodule.exists_finset_of_mem_iSup, IsIsotypic.linearEquiv_fun, integralClosure_le_span_dualBasis, LinearPMap.mem_domain_sSup_iff, finrank_span_finset_eq_card, LinearMap.exists_ne_zero_of_sSup_eq_top, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_fst, Submodule.comap_zero, LieSubmodule.instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket, finrank_span_set_eq_card, Submodule.linearProjOfIsCompl_apply_left, groupCohomology.toCocycles_comp_isoCocycles₁_hom, Valuation.leSubmodule_v_le_of_mem, Submodule.subtype_comp_inclusion, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, Submodule.mem_of_span_eq_top_of_smul_pow_mem, Affine.Simplex.orthogonalProjectionSpan_map, LinearMap.eqLocus_same, LinearMap.BilinForm.dualSubmoduleToDual_injective, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, ExteriorAlgebra.GradedAlgebra.liftι_eq, groupCohomology.isoCocycles₁_hom_comp_i_apply, Submodule.isScalarTower, Module.support_quotient, Module.Presentation.cokernelSolution_var, LinearMap.map_le_map_iff, Submodule.comap_inf, IsSemisimpleModule.submodule, Submodule.smul_def, AffineMap.restrict.bijective, Submodule.range_snd, Finsupp.mem_supported_support, isConnected_compl_of_one_lt_codim, Submodule.nonzero_mem_of_bot_lt, Submodule.bot_coe, Submodule.orthogonalBilin_le, RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule, groupCohomology.mem_cocycles₂_def, Submodule.mem_toAffineSubspace, RootPairing.root'In_corootSpanMem_eq_pairingIn, Submodule.set_smul_le_iff, RootPairing.rootForm_restrict_nondegenerate_of_ordered, Polynomial.degreeLT.instFreeSubtypeMemSubmodule, Submodule.algebraMap_mem, linearIndependent_option, Submodule.span_subset_span, Submodule.finrank_add_finrank_le_of_disjoint, GradedAlgHom.toGradedRingHom_ofClass, ZLattice.summable_norm_sub_inv_pow, tendsto_tsum_div_pow_atTop_integral, NumberField.canonicalEmbedding.mem_span_latticeBasis, Submodule.orthogonalDecomposition_symm_apply, Ideal.finrank_eq_finrank, Submodule.le_annihilator_iff, PeriodPair.hasSumLocallyUniformly_weierstrassP, Subalgebra.toSubmodule_injective, Submodule.vadd_def, LinearMap.subtype_comp_codRestrict, IsHilbertSum.mkInternal, exteriorPower.basis_apply, LinearMap.IsProj.subtype_comp_codRestrict, NumberField.Units.logEmbedding_fundSystem, Submodule.toIsOrderedAddMonoid, LinearMap.subtype_comp_restrict, linearIndepOn_iff_notMem_span, Submodule.mem_ideal_smul_span_iff_exists_sum, LinearMap.IsProj.codRestrict_apply_cod, LinearMap.BilinForm.isSkewAdjoint_bracket, Module.Basis.coe_span_apply, Submodule.span_sInf_le, RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', IsNoetherian.disjoint_partialSups_eventually_bot, Finsupp.restrictDom_apply, groupHomology.boundaries₂_le_cycles₂, Submodule.span_span_of_tower, rank_le_card_isVisible, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, exteriorPower.linearMap_ext_iff, IsLocalization.coeSubmodule_mul, vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints, Submodule.top_mul_eq_top_of_mul_eq_one, RootPairing.finrank_corootSpan_eq', AdicCompletion.AdicCauchySequence.mk_eq_mk, LinearMap.range_id, Submodule.mulMap_tmul, AddMonoidAlgebra.of'_mem_span, PeriodPair.coeff_weierstrassPExceptSeries, Valuation.mem_leSubmodule_iff, LinearMap.ker_eq_top, Submodule.subsingleton_iff_eq_bot, TensorProduct.eq_of_fg_of_subtype_eq', Submodule.comm_trans_lTensorOne, isNoetherian_submodule_right, Polynomial.toMatrix_sylvesterMap', RingTheory.Sequence.isWeaklyRegular_cons_iff', LinearMap.injOn_iff_surjOn, Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt, Submodule.exists_fg_le_eq_rTensor_inclusion, Submodule.smul_eq_map₂, Submodule.toConvexCone_inf, Polynomial.disjoint_ker_aeval_of_isCoprime, LinearMap.IsRefl.domRestrict, Ideal.mem_ofPolynomial, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, Affine.Simplex.finiteDimensional_direction_altitude, TensorProduct.range_mapIncl, LinearMap.BilinForm.ker_restrict_eq_of_codisjoint, IsIsotypic.isotypicComponents, Submodule.toLinearEquiv_orthogonalDecomposition_symm, Submodule.set_smul_span, Submodule.le_of_le_smul_of_le_jacobson_bot, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, LinearMap.ker_pi, Submodule.isInternal_prime_power_torsion_of_pid, Module.End.isNilpotent_restrict_genEigenspace_nat, IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe, Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Module.End.IsNilpotent.mapQ, Submodule.mem_localized', IsFractionRing.coeSubmodule_strictMono, Submodule.map_dualCoannihilator_le, Module.End.mem_invtSubmodule, Submodule.annihilator_quotient, RootPairing.EmbeddedG2.mem_span_of_mem_allRoots, LinearMap.injective_restrict_iff_disjoint, AdicCompletion.map_val_apply, Submodule.top_toAddSubmonoid, PeriodPair.derivWeierstrassPExcept_sub, IsLocalization.smul_mem_finsetIntegerMultiple_span, PointedCone.ofSubmodule_sSup, covBy_iff_quot_is_simple, lift_rank_map_le, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, LieSubmodule.bot_toSubmodule, MeasureTheory.norm_condExpL2_le, ModuleCat.epi_as_hom''_mkQ, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, ZSpan.floor_eq_self_of_mem, AffineSubspace.direction_inf_of_mem, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, Submodule.topologicalClosure_minimal, Submodule.instStrictConvexSpace, Submodule.tensorEquivSpan_apply_tmul, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, MonoidAlgebra.Submodule.exists_isCompl, Ideal.smul_top_eq_map, Submodule.linearMap_eq_zero_iff_of_eq_span, Submodule.localized₀_top, Rep.resCoindToHom_hom_apply_coe, Submodule.LinearDisjoint.bot_right, Submodule.coe_mapAlgEquiv_symm_apply, ContinuousLinearMap.ker_codRestrict, StrongDual.polarSubmodule_eq_setOf, Algebra.Extension.H1Cotangent.equiv_apply, groupCohomology.cocyclesIso₀_hom_comp_f, PeriodPair.ω₁_div_two_notMem_lattice, LinearMap.IsProj.mem_iff_map_id, RingTheory.Sequence.isWeaklyRegular_cons_iff, Module.Basis.mem_span, Module.Relations.Solution.surjective_π_iff_span_eq_top, Finsupp.supportedEquivFinsupp_symm_single, vsub_mem_vectorSpan, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LinearMap.IsProj.mem_invtSubmodule_iff, ImplicitFunctionData.isCompl_ker, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_left, PointedCone.coe_ofSubmodule, Rep.coindToInd_of_support_subset_orbit, Module.isTorsionBySet_quotient_set_smul, Submodule.mem_sup', span_fourier_closure_eq_top, groupCohomology.H1π_comp_map_assoc, LinearMap.ofIsCompl_symm, LieSubmodule.toSubmodule_le_toSubmodule, Submodule.addSubgroupClass, Polynomial.Sequence.span, Submodule.mul_comm, Submodule.re_inner_starProjection_eq_normSq, mem_pairSelfAdjointMatricesSubmodule, LieSubmodule.iSup_toSubmodule, groupHomology.mapCycles₁_comp_apply, DirectSum.decomposeAlgEquiv_symm_apply, Ring.coe_jacobson_quotient, Affine.Simplex.restrict_reindex, finiteDimensional_vectorSpan_range, LinearMap.le_ker_iff_comp_subtype_eq_zero, MeasureTheory.inner_condExpL2_left_eq_right, LinearEquiv.ker_le_fixedSubmodule_transvection, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, RootPairing.restrictScalars_coe_coroot, groupCohomology.π_comp_H0Iso_hom, Module.Finite.fg_top, exists_finrank_eq_sigPos_and_posDef, Submodule.addSubmonoidClass, ChevalleyThm.chevalley_polynomialC, Affine.Simplex.faceOppositeCentroid_restrict, sigNeg_isGreatest, Matrix.isSkewAdjoint_bracket, GradedTensorProduct.tmul_zero_coe_mul_coe_tmul, Submodule.linearEquiv_of_le_sSup, Submodule.linearProjOfIsCompl_apply_right, groupCohomology.π_comp_H1Iso_hom_assoc, Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero, exteriorPower.coe_basis, LinearMap.tensorKer_tmul, LinearMap.IsSymmetric.diagonalization_apply_self_apply, Submodule.dense_iff_topologicalClosure_eq_top, LinearMap.IsIdempotentElem.commute_iff, LinearPMap.domain_supSpanSingleton, finrank_vectorSpan_image_finset_le, EuclideanGeometry.orthogonalProjection_congr, Submodule.mem_colon', AffineSubspace.direction_le, Submodule.smul_bot, Submodule.mulMap_one_right_eq, LinearIndepOn.notMem_span, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, exteriorPower.ιMulti_family_linearIndependent_field, vsub_mem_vectorSpan_pair, Submodule.instIsCompactlyGenerated, ContinuousLinearEquiv.snd_equivOfRightInverse, AffineIsometryEquiv.ofTop_apply, mem_of_isSMulRegular_quotient_of_smul_mem, Submodule.comap_op_mul, Submodule.restrictScalars_eq_bot_iff, Submodule.span_setOf_mem_eq_top, LinearMap.range_eq_top_of_surjective, Submodule.toLinearEquiv_orthogonalDecomposition, Submodule.closedComplemented_top, DirectSum.IsInternal.baseChange, LinearPMap.mk_apply, Profinite.NobelingProof.Products.span_nil_eq_top, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, Subspace.dualRestrict_comp_dualLift, Submodule.restrictScalars_monotone, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, groupCohomology.mapCocycles₂_comp_i, LieSubalgebra.mem_map_submodule, Submodule.isOrtho_sup_right, RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm, Submodule.map₂_iSup_right, Orthonormal.codRestrict, Submodule.mapQ_apply, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, Submodule.dualQuotEquivDualAnnihilator_apply, TensorProduct.span_tmul_eq_top, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, Finsupp.instCountableSubtypeMemSubmoduleSpanRange, Submodule.Quotient.mk_add, ClosedSubmodule.toSubmodule_sup, Submodule.coe_toAddSubmonoid, Submodule.fst_sup_snd, LinearIndependent.linearCombination_repr, Submodule.mem_of_localization_maximal, exteriorPower.basis_repr_ne, Submodule.orthogonalProjection_mem_subspace_eq_self, LinearPMap.supSpanSingleton_apply_of_mem, Subbimodule.smul_mem', LinearMap.range_domRestrict_le_range, RootPairing.Base.root_mem_span_int, MvPolynomial.homogeneousComponent_mem, Submodule.toAddSubmonoid_injective, Submodule.factor_mk, Submodule.mk_eq_bot, ContinuousLinearMap.completeSpace_eqLocus, Polynomial.degreeLT_mono, Submodule.smul_mem_span_smul, DirectSum.isInternal_ne_bot_iff, Module.isTorsionBySet_quotient_ideal_smul, QuotSMulTop.equivTensorQuot_naturality, Module.Basis.mk_repr, Finsupp.span_single_eq_top, LinearMap.submoduleComap_apply_coe, Submodule.orthogonal_disjoint, finiteDimensional_direction_affineSpan_of_finite, Submodule.t3_quotient_of_isClosed, Module.End.independent_genEigenspace, Module.Flat.ker_lTensor_eq, MvPolynomial.weightedHomogeneousSubmodule_mul, Ideal.primaryComponent_sup, Module.Basis.groupSMul_span_eq_top, Module.Basis.ofZLatticeBasis_apply, Submodule.Quotient.instIsBoundedSMul, Submodule.mul_mem_mul, Submodule.codisjoint_span_image_of_codisjoint, groupCohomology.H0IsoOfIsTrivial_hom, Valuation.leSubmodule_monotone, Submodule.comap_op_pow, Submodule.ideal_span_singleton_smul, LinearMap.ofIsCompl_smul, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, Submodule.mem_orthogonal_singleton_iff_inner_right, NumberField.mixedEmbedding.mem_idealLattice, Submodule.top_eq_ofList_cons_smul_iff, BoxIntegral.unitPartition.mem_smul_span_iff, Submodule.quotDualCoannihilatorToDual_apply, Submodule.mul_one_div_le_one, OrthogonalFamily.of_pairwise, Submodule.injective_inclusionSpan, Module.End.invtSubmodule.disjoint_mk_iff, Submodule.IsLattice.rank', Submodule.restrictScalars_mul, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, Submodule.sub_mem_iff_left, LinearEquiv.map_mem_invtSubmodule_conj_iff, Span.repr_def, Submodule.map_iSup, LinearMap.mem_isPairSelfAdjointSubmodule, Module.End.eigenspaces_iSupIndep, bot_lt_isotypicComponent, Submodule.dualPairing_apply, Submodule.starProjection_singleton, TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_symm_apply_mk_tmul, Submodule.map₂_le_map₂, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom, Submodule.mem_iSup_iff_exists_finsupp, LinearMap.tensorEqLocusEquiv_apply, FractionalIdeal.isFractional_div_of_ne_zero, groupCohomology.coe_mapCocycles₁, LinearMap.IsRefl.ker_flip_eq_bot, LinearMap.domRestrict'_apply, Submodule.unique_quotient_iff_eq_top, groupHomology.mem_cycles₂_iff, Subrepresentation.mem_ofSubmodule'_iff, Fintype.mem_span_image_iff_exists_fun, lTensor.inverse_of_rightInverse_comp_lTensor, AdicCompletion.val_smul, DirectSum.IsInternal.submodule_iSupIndep, Affine.Simplex.restrict_map_restrict, RootPairing.invtRootSubmodule.eq_span_root, EuclideanGeometry.orthogonalProjection_contLinear, RootPairing.span_orbit_eq_top, Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson, ClosedSubmodule.coe_sSup, RootPairing.range_polarization_domRestrict_le_span_coroot, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, ContinuousLinearMap.ker_le_ker_iff_range_le_range, vectorSpan_eq_bot_iff_subsingleton, Module.End.genEigenspace_mem_invtSubmodule, RootPairing.finrank_range_polarization_eq_finrank_span_coroot, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, groupHomology.cyclesMap_comp_isoCycles₂_hom, Submodule.pi_univ_bot, Submodule.mem_smul_span_singleton, LinearMap.iSupIndep_map, LinearMap.fixedSubmodule_eq_top_iff, Submodule.restrictScalars_bot, Submodule.ClosedComplemented.exists_isClosed_isCompl, UnitAddTorus.mFourierSubalgebra_coe, AdicCompletion.incl_apply, Submodule.exists_le_ker_of_lt_top, Submodule.set_smul_mono_left, Submodule.coe_toBaseChange_tmul, ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule, Submodule.mem_invtSubmodule_reflection_of_mem, AffineSubspace.coe_subtypeA, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, RootPairing.invtRootSubmodule.bot_mem, LieSubalgebra.submodule_span_le_lieSpan, RootPairing.invtRootSubmodule.eq_top_iff, finrank_vectorSpan_le_iff_not_affineIndependent, groupCohomology.coboundariesToCocycles₁_apply, Submodule.LinearDisjoint.op, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, groupHomology.mapCycles₁_comp_assoc, AdicCompletion.val_smul_eq_evalₐ_smul, Submodule.eq_top_iff', Submodule.quotientPi_aux.map_smul, Submodule.mem_span_image_iff_exists_fun, Submodule.mem_iInf, LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.weierstrassP_coe, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, ZSpan.smul, Module.Basis.flag_le_ker_dual, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, IsArtinian.eventuallyConst_of_isArtinian, AffineSubspace.subtype_apply, Submodule.Quotient.instDiscreteMeasurableSpaceQuotient, Module.Basis.ofZLatticeComap_apply, Submodule.le_linearEquiv_of_sSup_eq_top, Submodule.FG.lTensor.directedSystem, Ideal.Filtration.smul_le, AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top, Module.supportDim_add_length_eq_supportDim_of_isRegular, Module.Basis.coe_mkFinConsOfLE, Submodule.comap_mono, Submodule.sub_mem_orthogonal_of_inner_left, Submodule.one_le_traceDual_one, Submodule.comap_le_comap_smul, rank_map_le, Submodule.subtypeₗᵢ_toContinuousLinearMap, Submodule.span_pow, FractionalIdeal.coe_le_coe, LinearMap.tensorKer_coe, LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton, Module.Baer.iff_surjective, Submodule.FG.exists_rTensor_fg_inclusion_eq, Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo, Submodule.finrank_quotient_add_finrank, Fintype.linearIndependent_iff', exists_le_isAssociatedPrime_of_isNoetherianRing, AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, isIsotypicOfType_submodule_iff, Submodule.map_span_le, IsAdicComplete.mkQ_comp_lift, Submodule.closure_subset_topologicalClosure_span, Module.exists_smul_eq_zero_and_mk_eq, Submodule.val_mulMap'_tmul, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, LinearMap.isUnit_iff_range_eq_top, Finsupp.mem_supported, CStarAlgebra.span_nonneg_inter_unitBall, Submodule.isSemisimple_torsionBy_of_irreducible, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, eq_isotypicComponent_iff, Module.End.genEigenspace_directed, Module.Basis.flag_last, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, RootPairing.coroot'In_rootSpanMem_eq_pairingIn, exteriorPower.alternatingMapLinearEquiv_ιMulti, Submodule.biSup_comap_eq_top_of_surjective, Submodule.coe_subtypeL', DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, Finsupp.mem_span_iff_linearCombination, Submodule.spanRank_toENat_eq_iInf_encard, Submodule.map₂_bot_right, LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt, Submodule.coe_sup, Polynomial.degreeLT.basis_val, Subspace.dualAnnihilator_dualAnnihilator_eq, selfAdjointPart_comp_subtype_skewAdjoint, Submodule.le_dualAnnihilator_dualCoannihilator, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, isotypicComponent_eq_top_iff, LinearMap.rank_eq_of_surjective, FractionalIdeal.coe_inf, Submodule.neg_top, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, Submodule.Quotient.instSubsingletonQuotient, Submodule.iSup_map_single_le, Module.jacobson_lt_top, lift_rank_range_of_injective, Ideal.mem_toCotangent_ker, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupHomology.δ₀_apply, groupCohomology.cocycles₂.d₂₃_apply, Submodule.smul_mono, Submodule.symmetric_isOrtho, Submodule.one_mem_div, LinearMap.iSup_range_single, isArtinian_iff_submodule_quotient, AffineSubspace.direction_eq_top_iff_of_nonempty, Submodule.pointwise_smul_def, Module.Grassmannian.rankAtStalk_eq, PeriodPair.hasSum_derivWeierstrassPExcept, RootPairing.span_coroot'_eq_top, Submodule.colon_finsetInf, Module.End.maxGenEigenspace_eq, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, LinearMap.map_injective, Subalgebra.mulMap_toLinearMap, Ideal.Filtration.mem_submodule, LinearMap.eventually_iSup_ker_pow_eq, Module.End.eigenspace_restrict_le_eigenspace, Representation.invtSubmodule.nontrivial_iff, LinearMap.IsSymmetric.directSum_decompose_apply, Submodule.mem_torsion_iff, Submodule.comap_fst, Submodule.linearProjOfIsCompl_comp_surjective_of_exact, Submodule.dualAnnihilator_map_dualMap_le, Submodule.sum_smul_mem, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_ker, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, le_comap_range_lTensor, Submodule.dualCopairing_eq, EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection, NonUnitalSubalgebra.toSubmodule_injective, LieSubmodule.mem_mk_iff', Submodule.mem_span_singleton_trans, RingTheory.Sequence.isRegular_cons_iff, groupHomology.isoCycles₁_inv_comp_iCycles_apply, Submodule.reflection_singleton_apply, rank_span_set, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, RootPairing.RootPositiveForm.zero_lt_posForm_iff, QuotSMulTop.equivTensorQuot_naturality_mk, Submodule.eq_zero_of_coe_mem_of_disjoint, Submodule.IsCompl.projection_apply_left, SetLike.Homogeneous.smul, IsLocalRing.map_mkQ_eq, eq_isotypicComponent_of_le, groupCohomology.map_H0Iso_hom_f_apply, LieModule.Cohomology.twoCochain_alt, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, groupCohomology.H0IsoOfIsTrivial_inv_apply, ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator, LinearMap.mem_skewAdjointSubmodule, Submodule.quotDualCoannihilatorToDual_nondegenerate, rank_bot, LinearPMap.mem_inverse_graph, Submodule.restrictScalars_top, Submodule.quotEquivOfEqBot_symm_apply, LieSubmodule.mem_toSubmodule, Submodule.mem_dualAnnihilator, Submodule.finrank_add_finrank_orthogonal', Submodule.mem_ideal_smul_span_iff_exists_sum', Submonoid.adjoin_eq_span_of_eq_span, LieSubmodule.disjoint_toSubmodule, EuclideanGeometry.Cospherical.inclusion_iff, linearIndepOn_id_union_iff, Submodule.smul_iSup', Submodule.ker_unitsToPic, Module.Presentation.cokernel_relation, coeff_minpolyDiv_sub_pow_mem_span, Submodule.le_of_localization_maximal, LieSubmodule.toSubmodule_injective, Submodule.dualAnnihilator_eq_top_iff, Submodule.orthogonal_eq_bot_iff, groupHomology.chains₁ToCoinvariantsKer_surjective, Submodule.inf_iInf, ZLattice.comap_discreteTopology, linearIndependent_iff_ker, adjoin_monomial_eq_reesAlgebra, InnerProductSpace.gramSchmidt_def, Ring.jacobson_smul_top_le, LinearMap.submoduleMap_coe_apply, ContinuousLinearMap.isComplete_ker, Module.End.mem_invtSubmodule_iff_mapsTo, Ideal.IsLasker.minimal, EuclideanGeometry.Cospherical.inclusion, AffineSubspace.linear_topEquiv, Submodule.prod_coe, Submodule.toLinearPMap_range, IsNoetherian.injective_of_surjective_of_submodule, Affine.Simplex.orthogonalProjectionSpan_eq_point, Submodule.coe_dualCoannihilator_span, QuadraticMap.Nondegenerate.radical_eq_bot, LieHom.quotKerEquivRange_toFun, LinearPMap.sub_domain, LinearMap.iInf_ker_proj, isSimpleModule_iff_isAtom, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, isFiniteLength_iff_exists_compositionSeries, FiniteDimensional.span_of_finite, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, Submodule.comap_smul_top_of_surjective, sigPos_isGreatest, mem_vectorSpan_iff_eq_weightedVSub, TensorProduct.map₂_eq_range_lift_comp_mapIncl, Module.End.mapsTo_genEigenspace_of_comm, Submodule.pow_smul_top_le, LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap, isArtinian_of_le, exteriorPower.ιMulti_span_of_span, DirectSum.IsInternal.collectedBasis_mem, groupHomology.cycles₁_eq_top_of_isTrivial, Submodule.biSup_comap_subtype_eq_top, MonoidAlgebra.of_mem_span_of_iff, Module.equiv_directSum_of_isTorsion, IsLinearTopology.hasBasis_open_submodule, LinearPMap.adjointAux_unique, QuotSMulTop.map_comp_mkQ, FractionalIdeal.isNoetherian_coeIdeal, RootPairing.injOn_dualMap_subtype_span_root_coroot, LinearMap.range_domRestrict_eq_range_iff, Submodule.subsingleton_iff, LinearMap.sub_mem_ker_iff, RootPairing.disjoint_corootSpan_ker_corootForm, TensorProduct.exists_finite_submodule_of_finite', Submodule.biSup_eq_range_dfinsupp_lsum, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, groupCohomology.mem_cocycles₁_def, Submodule.IsOrtho.orthogonalProjection_comp_subtypeL, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, IsIsotypic.submodule_linearEquiv_fun, RootPairing.restrictScalars_pairing, EuclideanGeometry.orthogonalProjection_map, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, Algebra.adjoin_span, Submodule.comap_map_sup_of_comap_le, QuadraticMap.le_radical_iff, LieModule.Cohomology.d₂₃_apply, Representation.Coinvariants.le_comap_ker, LieAlgebra.InvariantForm.restrict_nondegenerate, Submodule.le_self_mul_one_div, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf, LinearEquiv.fixedReduce_eq_one, exteriorPower.alternatingMapLinearEquiv_symm_map, LieIdeal.toInvtRootSubmodule_mono, LinearMap.span_singleton_sup_orthogonal_eq_top, Submodule.span_range_inclusion_restrictScalars_eq_top, isNoetherian_submodule, selfAdjointPart_comp_subtype_selfAdjoint, Submodule.le_div_iff_mul_le, AffineSubspace.vsub_mem_direction, HasStrictFDerivAt.eq_implicitFunctionOfComplemented, exteriorPower.instFree, Affine.Simplex.circumradius_restrict, HahnEmbedding.Partial.truncLT_mem_range_extendFun, Submodule.stabilizer_coe, IsSemisimpleModule.toComplementedLattice, Submodule.mulMap_comm, HahnEmbedding.Seed.baseEmbedding_strictMono, Module.Flat.out, RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, LieModule.Cohomology.d₁₂_apply_apply, Affine.Simplex.medial_restrict, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, ImplicitFunctionData.range_leftDeriv, FiniteDimensional.mem_span_of_iInf_ker_le_ker, Submodule.fg_biSup, Submodule.equivSubtypeMap_symm_apply, IsFractional.inf_right, Submodule.mem_prod, Submodule.botEquivPUnit_apply, Finsupp.iInf_ker_lapply_le_bot, LinearMap.ofIsComplProd_apply, Submodule.pointwise_smul_toAddSubgroup, AffineIndependent.finrank_vectorSpan_add_one, Submodule.coe_orthogonalDecomposition_symm, LinearMap.range_mkQ_comp, groupCohomology.mapCocycles₂_comp_i_apply, Projectivization.finrank_submodule, Submodule.ker_subtype, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, Submodule.map_comap_eq, MeasureTheory.aestronglyMeasurable_condExpL2, Submodule.orthogonalProjection_bot, rTensor.inverse_of_rightInverse_apply, LinearMap.ker_eq_bot, BoxIntegral.unitPartition.integralSum_eq_tsum_div, Submodule.linearProjOfIsCompl_apply_right', groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, ZLattice.module_finite, span_eq_top_localization_localization, LieSubmodule.isCompl_toSubmodule, LinearMap.iInf_ker_proj_le_iSup_range_single, Submodule.map_smul'', EuclideanGeometry.angle_orthogonalProjection_self, Submodule.mem_pi, Submodule.map_lt_map_of_le_of_sup_lt_sup, EuclideanGeometry.orthogonalProjection_apply_mem, DirectSum.bracket_apply_apply, ExteriorAlgebra.ιMulti_span, LinearMap.restrict_comp, isNoetherian_of_le, PointedCone.dual_ker, LinearMap.ker_smul', Submodule.coe_isComplEquivProj_symm_apply, Representation.card_inv_mul_sum_char_eq_finrank, AdicCompletion.pi_apply_coe, Ideal.Filtration.Stable.bounded_difference, EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq, LieSubalgebra.toSubmodule_le_toSubmodule, Submodule.finrank_add_inf_finrank_orthogonal, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, LinearMap.map_le_map_iff', LinearMap.ker_id, Submodule.exists_add_mem_mem_orthogonal, LieAlgebra.bracket_ofTwoCocycle, LinearMap.exact_subtype_mkQ, LieSubmodule.toSubmodule_orderEmbedding_apply, Submodule.coe_torsion', Submodule.prod_mono, Algebra.span_le_adjoin, AffineSubspace.coe_subtypeₐᵢ, Submodule.pow_add, Submodule.isClosed_topologicalClosure, PeriodPair.latticeBasis_zero, Module.Presentation.cokernel_R, Submodule.linearDisjoint_iff, Submodule.map_inf_comap_of_surjective, RingTheory.Sequence.isWeaklyRegular_iff_Fin, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, GradedTensorProduct.auxEquiv_one, LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, LinearMap.range_le_bot_iff, Submodule.span_singleton_eq_top_iff, Submodule.closedComplemented_bot, Submodule.mem_bot, AdicCompletion.val_add_apply, tendsto_card_div_pow_atTop_volume, Submodule.annihilator_iSup, Submodule.toLocalized₀_apply_coe, MvPolynomial.weightedDecomposition.decompose'_apply, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, Module.mapEvalEquiv_apply, LinearMap.IsSymm.domRestrict, Module.Basis.flag_mono, Submodule.neg_sup, Module.End.mem_eigenspace_intrinsicStar_iff, Subspace.finrank_dualCoannihilator_eq, Submodule.apply_mem_span_image_iff_mem_span, Submodule.sup_eq_range, AdicCompletion.ofPowSMul_ofValEqZero, Submodule.mem_map, Submodule.torsionBySet_le_torsionBySet_of_subset, Submodule.mem_div_iff_forall_mul_mem, Submodule.iInf_colon_iSup, LieSubmodule.lie_top_eq_of_span_sup_eq_top, AdicCompletion.smul_eval, MeasureTheory.condExpL2_indicator_ae_eq_smul, Finsupp.supported_inter, exteriorPower.ιMultiDual_apply_diag, Submodule.neg_iSup, Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, ModuleCat.smulShortComplex_X₃_isAddCommGroup, RootPairing.finrank_corootSpanIn_int, Submodule.span_smul_le, Submodule.sub_mem_sup, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, SModEq.zero, FractionalIdeal.div_of_ne_zero, Submodule.set_smul_eq_of_le, Submodule.smul_bot', groupCohomology.cocycles₂_map_one_fst, MvPolynomial.monomial_mul_mem_coeffsIn, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq, Finsupp.span_le_supported_biUnion_support, groupCohomology.mapCocycles₂_comp_i_assoc, LinearPMap.le_graph_iff, DirectSum.IsInternal.collectedBasis_coe, generator_maximal_submoduleImage_dvd, Submodule.le_orthogonal_orthogonal, Ideal.Filtration.sSup_N, Module.Dual.isCompl_ker_of_disjoint_of_ne_bot, Submodule.rank_quotient_add_rank, Ideal.toCotangent_range, RootPairing.IsIrreducible.eq_top_of_invtSubmodule_coreflection, Submodule.rank_le_spanRank, FractionalIdeal.mem_coeSubmodule, RootPairing.RootPositiveForm.posForm_apply_root_root_le_zero_iff, ZLattice.rank, ZLattice.tsum_norm_rpow_le, Subspace.finiteDimensional_quot_dualCoannihilator_iff, groupCohomology.H1IsoOfIsTrivial_inv_apply, ZSpan.quotientEquiv_apply_mk, LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker, OrderIso.setIsotypicComponents_apply, LinearIndependent.repr_eq_single, PeriodPair.ω₂_div_two_notMem_lattice, Module.FinitePresentation.equiv_quotient, Module.Presentation.cokernelSolution.isPresentation, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal, LieSubalgebra.mem_toSubmodule, Submodule.coe_toConvexCone, Module.Baer.ExtensionOf.is_extension, LinearMap.isCompl_range_inl_inr, FirstOrder.Field.lift_genericMonicPoly, Submodule.smul_mem_pointwise_smul, Submodule.instSMulCommClass, GradedTensorProduct.tmul_coe_mul_one_tmul, Ideal.adic_module_basis, LieSubmodule.sInf_toSubmodule, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, SubmodulesBasis.smul, isNoetherian_iSup, FractionalIdeal.coe_pow, PeriodPair.hasSum_derivWeierstrassP, groupHomology.mapCycles₁_id_comp_assoc, Module.Baer.ExtensionOf.dExt_iff, Subalgebra.mem_toSubmodule, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, rank_submodule_le_one_iff, PeriodPair.compl_lattice_diff_singleton_mem_nhds, AffineIndependent.card_le_finrank_succ, AdicCompletion.factor_eval_eq_evalₐ, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Coplanar.finrank_le_two, LocalizedModule.mem_ker_mkLinearMap_iff, Subalgebra.range_isScalarTower_toAlgHom, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule, Submodule.goursat, AffineSubspace.direction_affineSpan_insert, Submodule.coe_prodEquivOfIsCompl', Affine.Simplex.finrank_direction_altitude, LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot, IsCompactOperator.codRestrict, AffineSubspace.vectorSpan_union_of_mem_of_mem, LinearMap.range_zero, PeriodPair.hasSumLocallyUniformly_derivWeierstrassP, Submodule.orthogonal_orthogonal_monotone, Finsupp.supported_univ, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, Submodule.comap_iInf_map_of_injective, HahnEmbedding.Seed.strictMono_coeff, Submodule.subtypeₗᵢ_toLinearMap, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, Submodule.mem_span_finset, LinearMap.BilinMap.apply_apply_mem_of_mem_span, Module.Basis.sumQuot_repr_left, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, mem_skewAdjointMatricesSubmodule', LinearEquiv.ofSubmodules_apply, Submodule.quotientQuotientEquivQuotientAux_mk, RootPairing.mem_invtRootSubmodule_iff, LinearMap.lTensor_range, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, element_smul_restrictScalars, Submodule.topEquiv_apply, LinearMap.disjoint_inl_inr, Polynomial.degreeLT.addLinearEquiv_castAdd, Submodule.subtype_apply, GradedTensorProduct.tmul_coe_mul_coe_tmul, KaehlerDifferential.span_range_map_derivation_of_isLocalization, sSup_isotypicComponents, LinearEquiv.toSpanNonzeroSingleton_homothety, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, FiniteDimensional.finiteDimensional_quotient, MeasureTheory.integral_condExpL2_eq, Ideal.Filtration.inf_N, IsCompactOperator.restrict', Representation.Coinvariants.sub_mem_ker, Submodule.prod_le_iff, Profinite.NobelingProof.GoodProducts.spanFin, Submodule.dualAnnihilator_anti, Subrepresentation.toSubmodule_inf, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, finiteDimensional_vectorSpan_image_of_finite, RootPairing.instFiniteSubtypeMemSubmoduleRootSpanOfFinite, lTensor.inverse_of_rightInverse_apply, Algebra.toSubmodule_bot, Submodule.map_top, OrthogonalFamily.isInternal_iff_of_isComplete, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, Submodule.map_le_map_iff_of_injective, orzechProperty_iff, LinearIndependent.disjoint_span_image, ExteriorAlgebra.basis_eq_coe_basis, ContinuousLinearMap.isClosed_genEigenspace, Affine.Simplex.ninePointCircle_restrict, Submodule.mapQ_pow, Algebra.Extension.H1Cotangent.val_zero, Submodule.exists_forall_notMem_of_forall_ne_top, RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule, Submodule.submodule_eq_sSup_le_nonzero_spans, LinearMap.tensorKerEquivOfSurjective_symm_tmul, RootPairing.Base.coroot_mem_span_int, Submodule.smul_sup', HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq, Module.End.pow_restrict, Submodule.range_mkQ, groupCohomology.toCocycles_comp_isoCocycles₂_hom, LinearMap.IsProj.eq_conj_prodMap, LinearMap.tensorEqLocus_coe, coeSubmodule_differentIdeal, LinearMap.span_preimage_le, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_right, Submodule.mem_comap, DirectSum.coeLinearMap_lof, ContinuousLinearMap.iInf_ker_proj, Submodule.length_lt, Submodule.spanRank_range_le, Submodule.finrank_lt_finrank_of_lt, Submodule.map_unop_mul, LinearIsometry.isComplete_map_iff, Subrepresentation.toSubmodule_sup, LinearMap.mem_submoduleImage_of_le, Polynomial.degreeLT.addLinearEquiv_apply_fst, Submodule.mulLeftMap_apply, ZLattice.covolume.tendsto_card_div_pow, Submodule.finiteDimensional_finset_sup, coeSubmodule_differentIdeal_fractionRing, QuotSMulTop.map_surjective, LinearMap.restrict_commute, MeasureTheory.setIntegral_condExpL2_indicator, PeriodPair.mem_lattice, ModuleCat.imageIsoRange_hom_subtype, IsLinearTopology.hasBasis_submodule, stereographic_apply_neg, instCountable_of_discrete_submodule, OrthonormalBasis.orthogonalProjection_apply_eq_sum, groupHomology.mapCycles₁_comp_i, Submodule.ker_inl, LinearMap.toKerLocalized_isLocalizedModule, Submodule.submoduleOf_sup_of_le, Affine.Simplex.face_restrict, Submodule.isOpenQuotientMap_mkQ, rank_range_le, LieSubalgebra.engel_carrier, Submodule.finite_span_isCompactElement, Submodule.codisjoint_map, ClosedSubmodule.mem_toSubmodule_iff, Submodule.factor_eq_factor, DirectSum.coeLinearMap_of, ContinuousLinearMap.coe_equivRange, Submodule.topologicalClosure_map, Submodule.rank_le, Submodule.toConvexCone_top, Submodule.coe_prodEquivOfIsCompl, groupCohomology.shortComplexH0_f, DirectSum.coeLinearMap_eq_dfinsuppSum, HahnEmbedding.Partial.orderTop_eq_iff, LieSubmodule.coe_map_toEnd_le, Submodule.localized'_top, RootPairing.polarizationIn_Injective, finrank_vectorSpan_insert_le, LinearIsometryEquiv.coe_ofEq_apply, LinearMap.isUnit_iff_ker_eq_bot, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint, Submodule.norm_eq_iInf_iff_inner_eq_zero, Module.Basis.flag_zero, LinearIndependent.span_eq_top_of_card_eq_finrank', PeriodPair.analyticOnNhd_derivWeierstrassPExcept, AddSubmonoid.toNatSubmodule_toAddSubmonoid, groupCohomology.cocyclesOfIsCocycle₁_coe, Subspace.dualPairing_nondegenerate, Affine.Simplex.interior_restrict, MvPolynomial.degreesLE_nsmul, GradedAlgebra.algebraMap_apply, vsub_rev_mem_vectorSpan_pair, LinearMap.bot_lt_ker_of_det_eq_zero, monomial_mem_adjoin_monomial, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, Submodule.eq_top_of_nonempty_interior', Submodule.iSup_mul, AddSubmonoid.toNatSubmodule_closure, Submodule.localized'_iSup, DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate, Algebra.sInf_toSubmodule, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, Submodule.mul_mem_smul_iff, LieSubmodule.mk_eq_top_iff, RootPairing.finrank_rootSpanIn_int, AddMonoidAlgebra.decomposeAux_coe, Submodule.Quotient.completeSpace, CStarAlgebra.span_nonneg, groupCohomology.coboundaries₂_le_cocycles₂, Representation.invtSubmodule.coe_top, LinearMap.ker_rangeRestrict, Submodule.FG.eq_bot_of_le_jacobson_smul, CliffordAlgebra.evenOdd.gradedMonoid, Submodule.smul_subset_smul, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, Submodule.localized'_inf, FiniteDimensional.RCLike.properSpace_submodule, LieIdeal.rootSpan_mem_invtRootSubmodule, EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq, range_stereographic_symm, AffineSubspace.inclusion_linear, Hausdorffification.instIsHausdorff, AddMonoidAlgebra.gradeBy.isInternal, Submodule.linearMap_qext_iff, Submodule.traceDual_top', LinearMap.compMultilinearMap_codRestrict, MvPolynomial.mul_X_mem_coeffsIn, Module.Flat.iff_rTensor_injective, ChevalleyThm.chevalley_mvPolynomialC, HasStrictFDerivAt.to_implicitFunctionOfComplemented, EuclideanGeometry.orthogonalProjection_apply', LinearEquiv.mem_fixedSubmodule_transvection_iff, AddSubgroup.toZModSubmodule_toAddSubgroup, CliffordAlgebra.involute_mem_evenOdd_iff, Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, isOpenEmbedding_stereographic_symm, HahnEmbedding.Partial.extendFun_strictMono, TensorProduct.Algebra.exists_of_fg, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, Set.Finite.submoduleSpan, Rep.coindVEquiv_symm_apply_coe, exists_extension_of_le_sublinear, EuclideanGeometry.Sphere.coe_secondInter, Ideal.map_includeRight_eq, Submodule.inf_genEigenspace, Submodule.finiteDimensional_sup, isIsotypic_submodule_iff, Submodule.smul_le_self_of_tower, AdicCompletion.mkₐ_apply_coe, finiteDimensional_direction_map, Submodule.dualCoannihilator_iSup_eq, Module.comap_eval_surjective, LinearMap.map_coprod_prod, Submodule.span_le_restrictScalars, Submodule.torsionBy_torsionBy_eq_top, Submodule.LinearDisjoint.rank_inf_le_one_of_flat, Submodule.smul_mem_span_smul_of_mem, Submodule.sum_mem, linearIndependent_sum, Submodule.coe_span_smul, TensorProduct.exists_finite_submodule_left_of_setFinite, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, LinearEquiv.mem_dilatransvections_iff_rank, ModuleCat.imageIsoRange_inv_image_ι_apply, Submodule.exists_le_ker_of_notMem, basisOfLinearIndependentOfCardEqFinrank_repr_apply, mem_pairSelfAdjointMatricesSubmodule', ContinuousLinearMap.isClosed_ker, Submodule.height_strictMono, MvPolynomial.X_mul_mem_coeffsIn, LinearEquiv.fixedSubmodule_eq_top_iff, EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, LinearMap.IsProj.isCompl, Submodule.span_attach_biUnion, Ideal.Quotient.span_singleton_one, Submodule.span_eq_bot, Submodule.strictMono_comap_prod_map, Matrix.cRank_toNat_eq_finrank, Module.End.map_genEigenrange_le, Submodule.mem_annihilator', Submodule.Quotient.equiv_symm, Submodule.le_one_toAddSubmonoid, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, Submodule.span_mul_span, Submodule.starProjection_top', AdicCompletion.isAdicCauchy_iff, groupCohomology.coboundaries₂.val_eq_coe, RootPairing.PolarizationIn_eq, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, Submodule.adjoint_subtypeL, LinearMap.BilinForm.orthogonal_eq_bot_iff, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Submodule.instIsTwoSidedColonCoe, IsCoercive.range_eq_top, Submodule.map_bot, Submodule.ext_iff, LinearMap.range_eq_top_of_cancel, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, Pi.mem_spanSubset_iff, Submodule.le_traceDual_traceDual, Submodule.dualRestrict_ker_eq_dualAnnihilator, LinearIsometry.equivRange_apply_coe, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, Submodule.mem_left_iff_eq_zero_of_disjoint, FiniteDimensional.span_finset, Submodule.reflection_orthogonalComplement_singleton_eq_neg, Submodule.comap_iSup_map_of_injective, lipschitzGroup.conjAct_smul_ι_mem_range_ι, Subalgebra.finrank_toSubmodule, LinearMap.surjective_range_liftQ, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, ZLattice.tsumNormRPowBound_spec, LinearIsometryEquiv.reflections_generate_dim_aux, IsLocalRing.map_tensorProduct_mk_eq_top, MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring, Submodule.map₂_iSup_left, AdicCompletion.val_sum, IsLocalization.coeSubmodule_mono, Affine.Triangle.dist_circumcenter_reflection_orthocenter, MeasureTheory.norm_condExpL2_coe_le, MvPolynomial.degreesLE_add, LinearIndependent.iSupIndep_span_singleton, isArtinian_span_of_finite, Submodule.restrictScalars_lt, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, IsIsotypic.isotypicComponent, Submodule.toBaseChange_surjective, LinearMap.finrank_range_of_inj, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, LinearMap.restrict_sub, Ideal.pi_mkQ_surjective, LinearMap.iSup_range_single_eq_iInf_ker_proj, Subrepresentation.toSubmodule_injective, Module.End.IsSemisimple.iSup_eigenspace_eq_top, LinearMap.toPMap_apply, groupCohomology.d₁₂_apply_mem_cocycles₂, Rep.invariantsAdjunction_unit_app, DenseRange.topologicalClosure_map_submodule, groupHomology.mapCycles₂_id_comp, IsNoetherian.wf, Finsupp.supported_comap_lmapDomain, Submodule.coe_linearProjOfIsCompl_apply, Submodule.inclusion_apply, UniqueDiffWithinAt.dense_tangentConeAt, LinearMap.linearProjOfIsCompl_apply_right, Subalgebra.isIdempotentElem_toSubmodule, ArchimedeanClass.mem_ball_iff, groupCohomology.d₀₁_apply_mem_cocycles₁, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, Submodule.mem_smul_iff_inv_mul_mem, LinearEquiv.ofLeftInverse_symm_apply, Submodule.map_sup, LinearMap.range_rangeRestrict, isNoetherian_iff_submodule_quotient, ZSpan.repr_ceil_apply, PowerSeries.coe_hasEvalIdeal, LinearMap.IsPerfectCompl.isCompl_right, ZLattice.comap_equiv_apply, Submodule.surjective_tensorToSpan, FractionalIdeal.coe_nsmul, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, Submodule.mem_torsionBySet_iff, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.Quotient.mk_sub, Matrix.ker_mulVecLin_eq_bot_iff, Submodule.torsion_torsion_eq_top, LinearIsometryEquiv.ofTop_toLinearEquiv, Convex.span_tangentConeAt, finrank_span_le_card, Submodule.coe_ofClass, vectorSpan_empty, span_coeff_minpolyDiv, IsHausdorff.iInf_pow_smul, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, Submodule.isLocalizedModule, lTensor.inverse_apply, Submodule.range_subtypeL, Submodule.biInf_comap_proj, Module.isTorsionBySet_iff_torsionBySet_eq_top, Submodule.botEquivPUnit_symm_apply, Module.Basis.addSubgroupOfClosure_repr_apply, IsLocalization.coeSubmodule_bot, IsFractional.mul, isSMulRegular_submodule_iff_right_eq_zero_of_smul, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank, groupCohomology.subtype_comp_d₀₁_apply, Module.Basis.span_repr_eq_single, PeriodPair.isClosed_lattice, linearIndependent_fin_cons, Module.length_top, SymmetricPower.span_tprod_eq_top, Submodule.span_range_inclusion_eq_top, Submodule.toAddSubmonoid_strictMono, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, contDiffOn_stereoToFun, SchauderBasis.finrank_range_proj, spinGroup.conjAct_smul_ι_mem_range_ι, Submodule.image_span_subset_span, Submodule.prod_top, MonoidAlgebra.mem_span_support, GradedTensorProduct.auxEquiv_symm_one, FractionalIdeal.coe_natCast, groupCohomology.H2π_eq_iff, le_sigPos_of_posDef, NumberField.det_basisOfFractionalIdeal_eq_absNorm, GradedTensorProduct.auxEquiv_comm, LinearMap.comap_leq_ker_subToSupQuotient, QuadraticForm.sigPos_add_sigNeg_add_radical, Rep.coindFunctorIso_inv_app_hom_toFun_coe, Submodule.LinearDisjoint.linearIndependent_right_of_flat, HilbertBasis.hasSum_orthogonalProjection, LieModule.coe_genWeightSpaceOf_zero, Submodule.smul_coe_torsionBy, LinearMap.rTensor_injective_iff_subtype, MeasureTheory.mem_lpMeas_indicatorConstLp, stereoInvFun_apply, Submodule.map_mkQ_eq_top, Submodule.disjoint_span_singleton, Submodule.eq_top_of_disjoint, Submodule.eq_bot_of_subsingleton, HahnEmbedding.IsPartial.strictMono, collinear_iff_finrank_le_one, Module.Flat.torsion_eq_bot, Submodule.isOrtho_sSup_right, LinearMap.subtype_compAlternatingMap_codRestrict, Submodule.iSup_span, groupCohomology.cocycles₂_map_one_snd, Submodule.mem_set_smul_def, Module.End.invtSubmodule.isCompl_iff, groupCohomology.δ₁_apply, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, LinearIsometryEquiv.ofTop_symm_apply_coe, Submodule.map_eq_top_iff, LieDerivation.ofGradingSum_of, LinearMap.submoduleImage_apply_of_le, Submodule.snd_map_fst, Algebra.top_toSubmodule, LinearRecurrence.solSpace_rank, Submodule.one_le_one_div, Module.coe_length, LieSubalgebra.coe_toSubmodule, LinearEquiv.ofSubmodule'_symm_apply, groupHomology.toCycles_comp_isoCycles₁_hom_apply, AffineIsometryEquiv.coe_ofEq_apply, IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp, Submodule.isTorsion'_iff_torsion'_eq_top, Submodule.closed_of_finiteDimensional, Representation.mem_invariants_iff_of_forall_mem_zpowers, spinGroup.involute_act_ι_mem_range_ι, Affine.Simplex.altitude_restrict_eq_comap_subtype, MeasureTheory.lintegral_nnnorm_condExpL2_le, PeriodPair.periodic_derivWeierstrassP, exteriorPower.finrank_eq, ContinuousLinearMap.eqOn_closure_span, AffineSubspace.isometryEquivMap.toAffineMap_eq, groupHomology.mapCycles₂_comp_i, AffineSubspace.signedInfDist_eq_signedDist_of_mem, Polynomial.degreeLT.addLinearEquiv_apply_snd, Submodule.span_singleton_algebraMap_of_isUnit, LinearPMap.supSpanSingleton_apply_mk_of_mem, Finsupp.mem_submodule_iff, KaehlerDifferential.span_range_derivation, ModuleCat.range_eq_top_of_epi, groupCohomology.map_H0Iso_hom_f, Submodule.mem_span_singleton, LinearMap.finrank_genEigenspace_le, Submodule.codisjoint_iff_exists_add_eq, Module.Basis.sumQuot_repr_inl, LinearMap.IsSymmetric.diagonalization_symm_apply, Submodule.eq_smul_of_le_smul_of_le_jacobson, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff, isArtinian_of_quotient_of_artinian, ContinuousLinearMap.coe_codRestrict, groupHomology.boundariesOfIsBoundary₁_coe, Module.Basis.isMaxChain_range_flag, LieSubalgebra.sInf_toSubmodule, Submodule.eq_bot_of_localization_maximal, LieModule.weight_vector_multiplication, Affine.Simplex.signedInfDist_apply_self, spinGroup.conjAct_smul_range_ι, Representation.mem_invariants, LinearMap.quotientInfEquivSupQuotient_apply_mk, KaehlerDifferential.kerTotal_mkQ_single_add, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, AdicCompletion.range_eval, finiteDimensional_vectorSpan_of_finite, Module.End.iSup_genEigenspace_eq, Ideal.Quotient.smul_top, Submodule.finiteQuotient_iff, groupCohomology.π_comp_H1Iso_hom, LinearMap.ker_toSpanSingleton, LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg, IsSimpleModule.isAtom, RootPairing.corootSpanMem_reflectionPerm_self, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, Submodule.pointwise_smul_toAddSubmonoid, Module.isTorsionBySet_span_singleton_iff, AdicCompletion.val_neg_apply, Module.Basis.flag_le_ker_coord, CStarAlgebra.span_nonneg_inter_unitClosedBall, Function.Exact.exact_mapQ_iff, Submodule.iSup_dualAnnihilator_le_iInf, Submodule.LinearDisjoint.one_left, Module.End.genEigenspace_inf_le_add, CliffordAlgebra.range_ι_le_evenOdd_one, Submodule.restrictScalars_image_smul_eq, Module.End.eigenspace_restrict_eq_bot, Submodule.comap_iInf, LinearIsometryEquiv.reflections_generate, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, Subrepresentation.mem_asSubmodule'_iff, exteriorPower.map_apply_ιMulti_family, Module.End.eigenspace_le_genEigenspace, AddSubgroup.toIntSubmodule_symm, LinearMap.range_eq_bot, NumberField.mixedEmbedding.span_idealLatticeBasis, Submodule.coe_mk, HomogeneousSubmodule.mem_toSubmodule_iff, Module.Quotient.mk_smul_mk, Submodule.fst_inf_snd, ExteriorAlgebra.ιMulti_range, RootPairing.invtRootSubmodule.le_ker_coroot', Submodule.bot_smul, Submodule.map₂_bot_left, differentialIdeal_le_iff, ClosedSubmodule.toSubmodule_iSup, Submodule.sum_mem_iSup, AffineEquiv.linear_ofEq, LinearMap.submoduleOf_span_singleton_of_mem, Submodule.norm_orthogonalProjection_apply_le, instPolynormableSpaceSubtypeMemSubmodule, Submodule.top_toAddSubgroup, HahnEmbedding.Partial.exists_sub_mem_ball, HasStrictFDerivAt.map_implicitFunction_eq, AffineSubspace.coe_direction_eq_vsub_set, Module.Basis.toDual_ker, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, GradedAlgebra.proj_recompose, Field.span_map_pow_expChar_pow_eq_top_of_isSeparable, Submodule.mem_span_iff_exists_finset_subset, PointedCone.ofSubmodule_sInf, Submodule.mem_span_mul_finite_of_mem_mul, Submodule.apply_coe_mem_map, OrthonormalBasis.starProjection_eq_sum_rankOne, HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum, LinearMap.BilinForm.apply_apply_same_eq_zero_iff, Submodule.mem_iSup_iff_exists_dfinsupp, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, FDRep.average_char_eq_finrank_invariants, IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime, Submodule.singleton_span_isCompactElement, Submodule.span_prod_le, top_isPrincipal, Ideal.Filtration.top_N, Submodule.span_range_eq_iSup, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, AffineIsometryEquiv.ofTop_symm_apply_coe, LinearIndepOn.subset_span_extend, isArtinian_range, LinearMap.disjoint_ker, TopologicalSpace.IsSeparable.span, MvPolynomial.restrictSupport_univ, TensorProduct.inner_mapIncl_mapIncl, Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes, RootPairing.toLinearMap_apply_PolarizationIn, PointedCone.lineal_eq_sSup, Ideal.Filtration.sInf_N, exteriorPower.zeroEquiv_naturality, Collinear.finiteDimensional_direction_affineSpan, finiteDimensional_direction_affineSpan_insert_set, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, TensorProduct.exists_finite_submodule_right_of_setFinite, HahnEmbedding.IsPartial.truncLT_mem_range, Submodule.restrictScalars_le, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply_ker, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, Affine.Simplex.orthogonalProjectionSpan_congr, LinearIndependent.linearCombinationEquiv_apply_coe, Submodule.toAddSubgroup_mono, Polynomial.adjSylvester_comp_sylveserMap, Ideal.Filtration.iInf_N, Submodule.subset_span_trans, Module.length_eq_top_iff_infiniteDimensionalOrder, Submodule.dualCoannihilator_anti, FractionalIdeal.coeToSubmodule_eq_bot, Submodule.mapsTo_smul_closure, Submodule.eq_top_of_isLocalized₀_span, Submodule.lt_of_le_of_finrank_lt_finrank, Submodule.toSubalgebra_toSubmodule, iSupIndep_iff_linearIndependent_of_ne_zero, LieModule.lie_mem_maxGenEigenspace_toEnd, Submodule.iSup_eq_range_dfinsupp_lsum, Module.Basis.span_apply, LieModule.Cohomology.twoCochain_skew, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, NonUnitalAlgebra.toSubmodule_bot, Submodule.norm_eq_iInf_iff_real_inner_eq_zero, Submodule.mapQ_zero, Submodule.IsMinimalPrimaryDecomposition.inf_eq, LinearMap.ker_codRestrict, AffineSubspace.mem_direction_iff_eq_vsub, groupCohomology.cocycles₂.coe_mk, Module.Finite.quotient, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, DFinsupp.iSup_range_lsingle, ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, LinearMap.IsSymmetric.restrict_invariant, AdicCompletion.transitionMap_comp_eval, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, Submodule.isCoatom_map_of_ker_le, Submodule.localized₀_bot, RootPairing.instFiniteSubtypeMemSubmoduleCorootSpanOfFinite, AffineIsometryEquiv.ofEq_symm, traceForm_dualSubmodule_adjoin, ContinuousLinearMap.equivRange_symm_apply, FractionalIdeal.adjoinIntegral_coe, FractionalIdeal.coe_dual_one, RootPairing.finrank_corootSpanIn, LinearIndependent.linearCombination_comp_repr, Ideal.quotientToQuotientRangePowQuotSucc_mk, CliffordAlgebra.one_le_evenOdd_zero, ModuleCat.smulShortComplex_g, Submodule.coe_restrictScalars, LinearPMap.mkSpanSingleton'_apply_self, Submodule.bot_toAddSubmonoid, Subalgebra.mul_toSubmodule, Submodule.restrictScalars_map_smul_eq, Representation.coe_coindV, Submodule.coe_inclusion, LinearIsometry.extend_apply, LinearPMap.HasCore.le_domain, Algebra.adjoin_nonUnitalSubalgebra_eq_span, LinearPMap.inverse_isClosable_iff, Submodule.map_inf_eq_map_inf_comap, instLocallyConvexSpaceSubtypeMemSubmodule, Polynomial.degreeLT.instFiniteSubtypeMemSubmodule, ArchimedeanClass.ball_le_closedBall, Submodule.isOrtho_top_left, atom_iff_nonzero_span, Submodule.instMulLeftMono, Submodule.finrank_strictMono, Polynomial.sup_aeval_range_eq_top_of_isCoprime, Module.End.IsSemisimple.restrict, IsFractional.sup, exists_linearIndepOn_extension, Submodule.comap_coe, OrthogonalFamily.isInternal_iff, LinearMap.BilinForm.mem_dualSubmodule, asymptoticCone_affineSubspace, Submodule.linearEquiv_det_reflection, MvPolynomial.map_restrict_dom_evalₗ, groupCohomology.instEpiModuleCatH1π, Polynomial.coeff_modByMonic_mem_pow_natDegree_mul, PeriodPair.differentiableOn_derivWeierstrassP, LinearPMap.apply_comp_inclusion, Submodule.subsingleton_quotient_iff_eq_top, PeriodPair.weierstrassPExcept_def, Submodule.snd_map_snd, Submodule.span_val_image_eq_iff, LinearMap.ker_prod_ker_le_ker_coprod, Module.FinitePresentation.exists_fin, LieSubmodule.toEnd_comp_subtype_mem, Submodule.coe_quotEquivOfEqBot_symm, LieSubmodule.top_toSubmodule, GradedTensorProduct.tmul_one_mul_coe_tmul, Submodule.pi_mono, Submodule.mk_mem_projectivization_iff, Submodule.coe_pointwise_smul, CliffordAlgebra.submodule_comap_mul_reverse, Submodule.prod_eq_bot_iff, Coplanar.finiteDimensional_direction_affineSpan, IsSemisimpleModule.sup, Module.jacobson_pi_le, Matrix.rank_eq_finrank_range_toLin, exists_compositionSeries_of_isNoetherian_isArtinian, iSupIndep.subtype_ne_bot_le_finrank, RKHS.kerFun_dense, Submodule.annihilator_smul, Submodule.jacobson_smul_lt_top, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, groupCohomology.H2π_comp_map, Finsupp.codisjoint_supported_supported, Matrix.eRank_toNat_eq_finrank, LinearPMap.sSup_apply, Submodule.map_strictMono_of_injective, CharacterModule.intSpanEquivQuotAddOrderOf_apply, GradedAlgHom.instGradedFunLikeSubmodule, isNoetherian_iff_fg_wellFounded, QuadraticMap.Equivalent.rank_radical_eq, Submodule.pow_succ, Finsupp.supported_union, groupHomology.π_comp_H2Iso_hom, AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection, stereoToFun_apply, uniqueDiffWithinAt_iff, Submodule.IsPrincipal.mem_iff_eq_smul_generator, Submodule.sub_starProjection_mem_orthogonal, LinearPMap.snd_apply, Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero, Submodule.IsLattice.smul, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, NumberField.mixedEmbedding.mem_span_latticeBasis, exteriorPower.ιMulti_apply_coe, TensorAlgebra.ι_range_disjoint_one, affineIndependent_iff_not_finrank_vectorSpan_le, CliffordAlgebra.submodule_map_pow_reverse, Submodule.isCoatom_comap_iff, Submodule.coe_tensorSpanEquivSpan_apply_tmul, Submodule.annihilator_map_mkQ_eq_colon, LieSubmodule.mem_baseChange_iff, SModEq.sub_mem, Submodule.FG.lTensor.directLimit_apply', PowerBasis.mem_span_pow', Submodule.dualRestrict_def, ContinuousLinearMap.coe_projKerOfRightInverse_apply, Submodule.IsLattice.inf, Submodule.span_eq_top_of_span_eq_top, Rep.coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, Submodule.dualCoannihilator_bot, Module.Basis.SmithNormalForm.snf, Submodule.pi_empty, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, ClosedSubmodule.orthogonal_eq_inter, EuclideanGeometry.Sphere.orthogonalProjection_orthRadius_center, LinearMap.restrict_eq_codRestrict_domRestrict, Finsupp.supported_iInter, AdicCompletion.coe_eval, exists_finrank_eq_sigNeg_and_negDef, SetLike.homogeneous_zero_submodule, Submodule.mul_sup, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, RootPairing.invtRootSubmodule.top_mem, Submodule.dualCoannihilator_top, MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum, Submodule.mul_comm_of_commute, LinearMap.separatingRight_iff_flip_ker_eq_bot, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one, Submodule.FG.rTensor.directLimit_apply, groupCohomology.isoCocycles₂_hom_comp_i, EuclideanGeometry.orthogonalProjection_subtype, LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, Submodule.coe_orthogonalDecomposition, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, rank_submodule_le_one_iff', Submodule.mem_singleton_set_smul, groupCohomology.π_comp_H0Iso_hom_apply, LinearMap.sup_range_inl_inr, Submodule.map_unop_pow, IsSMulRegular.submodule, finiteDimensional_direction_affineSpan_insert, Submodule.ker_liftQ_eq_bot', Rep.subtype_hom_toFun, QuadraticForm.finrank_radical_of_equiv_weightedSumSquares, StrongDual.polarSubmodule_eq_polar, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, Submodule.orderIsoMapComap_apply', Submodule.finrank_orthogonal_span_singleton, IsLocalizedModule.subsingleton_iff_ker_eq_top, Submodule.inclusionSpan_apply_coe, groupHomology.coe_mapCycles₂, coe_topologicalNilradical, FractionalIdeal.isFractional_adjoin_integral, Submodule.small_span_singleton, Submodule.comap_subtype_self, LieSubmodule.iInf_toSubmodule, exteriorPower.oneEquiv_naturality, RieszExtension.exists_top, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, ExteriorAlgebra.ι_range_disjoint_one, LinearMap.span_singleton_sup_ker_eq_top, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, LinearMap.IsPerfectCompl.left_top_iff, Submodule.one_le_finrank_iff, IsLocalizedModule.mem_ker_iff, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, Module.Basis.eval_range, LinearEquiv.eq_bot_of_equiv, Submodule.isOrtho_iSup_left, groupHomology.H1π_comp_map_apply, AdicCompletion.val_mul, Affine.Simplex.ExcenterExists.excenter_restrict, LinearMap.mem_eqLocus, Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem, Submodule.localized₀_smul, Submodule.annihilator_bot, RootPairing.isIrreducible_iff, RootPairing.GeckConstruction.span_range_h'_eq_top, Submodule.norm_subtypeL, SModEq.smul', RootPairing.posRootForm_posForm_pos_of_ne_zero, Submodule.mem_orthogonal', Submodule.span_singleton_eq_bot, Projectivization.independent_iff_iSupIndep, Submodule.smul_le_smul, Submodule.Quotient.mk_smul, mem_integralClosure_iff_mem_fg, Subrepresentation.submoduleSubrepresentationOrderIso_apply, LinearPMap.sub_apply, Submodule.span_univ, Module.Flat.eqLocus_lTensor_eq, LinearMap.lift_rank_eq_of_surjective, Subspace.dualRestrict_leftInverse, TensorProduct.exists_finite_submodule_left_of_finite, nonzero_span_atom, smul_top_inf_eq_smul_of_isSMulRegular_on_quot, Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, ModuleCat.span_exact, Submodule.IsCompl.projection_eq_self_iff, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne, AffineSubspace.toContinuousAffineMap_subtypeₐᵢ, Submodule.rank_mono, LieModule.Cohomology.mem_twoCochain_iff, Submodule.mkQ_apply, Submodule.toIntSubmodule_toAddSubgroup, ContinuousLinearMap.IsIdempotentElem.TFAE, LinearMap.ker_noncommProd_eq_of_supIndep_ker, LinearMap.comap_codRestrict, ContinuousLinearMap.coe_rangeRestrict, Submodule.comap_finsetInf, Submodule.toAddSubmonoid_mono, Submodule.setLike.coe_galgebra_toFun, Submodule.le_topologicalClosure, Submodule.norm_sq_eq_add_norm_sq_projection, finiteDimensional_direction_affineSpan_range, IsArtinian.monotone_stabilizes, Polynomial.det_taylorLinearEquiv_toLinearMap, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq, LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one, Submodule.traceDual_le_span_map_traceDual, linearDepOn_iff, ContinuousLinearMap.equivRange_symm_toLinearEquiv, MvPolynomial.decompose'_apply, LinearMap.comap_injective, Submodule.orthogonal_gc, Submodule.comap_sup_map_of_injective, AdicCompletion.mk_smul_mk, Submodule.top_colon, EuclideanGeometry.orthogonalProjection_vadd_eq_self, Submodule.mem_colon_iff_le, LocalizedModule.subsingleton_iff_ker_eq_top, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, LinearMap.ker_toSpanSingleton_eq_bot_iff, Submodule.baseChange_bot, Submodule.IsLocalizedModule.localized₀FrameHom_apply, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, LinearEquiv.ofInjective_apply, FractionalIdeal.coe_mk, Module.length_submodule, FiniteArchimedeanClass.mem_ball_iff, Submodule.comm_trans_rTensorOne, DirectSum.decompose_symm_bracket, Submodule.starProjection_apply, OrzechProperty.injective_of_surjective_of_submodule, Submodule.card_quotient_mul_card_quotient, IsFractional.div_of_nonzero, FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target, Submodule.factor_comp, Submodule.coe_finsetInf, ZLattice.summable_norm_rpow, linearIndependent_span, LieSubalgebra.toSubmodule_injective, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, span_range_eq_top_iff_surjective_fintypeLinearCombination, Submodule.mem_span_set, MatrixModCat.toModuleCat_obj_carrier, Subspace.flip_quotDualCoannihilatorToDual_bijective, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, Submodule.restrictScalars_sSup, linearIndepOn_iff_disjoint, Submodule.apply_mem_map₂, Submodule.comap_equiv_self_of_inj_of_le_apply, Submodule.eq_bot_of_isLocalized'_span, rank_quotient_add_rank_of_isDomain, pinGroup.conjAct_smul_ι_mem_range_ι, groupCohomology.cocycles₁_map_inv, Module.Basis.sumQuot_repr_inl_of_mem, Submodule.exists_fg_le_subset_range_rTensor_subtype, DirectSum.coeAlgHom_of, Submodule.prod_span, TensorProduct.rTensor_injective_of_forall_vanishesTrivially, isArtinian_of_fg_of_artinian, Submodule.set_smul_eq_map, Submodule.nontrivial_iff, Affine.Triangle.dist_orthocenter_reflection_circumcenter, Submodule.comap_injective_of_surjective, groupCohomology.mapCocycles₁_one, Submodule.toAddSubgroup_injective, Subalgebra.adjoin_eq_span_basis, Ideal.IsLasker.exists_isMinimalPrimaryDecomposition, Polynomial.aeval_apply_smul_mem_of_le_comap, LinearMap.coe_range, EuclideanGeometry.oangle_orthogonalProjection_self, Submodule.isCoatom_comap_or_eq_top, Module.End.invtSubmodule.one, Affine.Simplex.map_altitude_restrict, LinearMap.mem_span_iff_continuous_of_finite, Submodule.top_orthogonal_eq_bot, Affine.Simplex.faceOpposite_restrict, groupHomology.H2π_comp_map_assoc, Submodule.neg_mem_iff, Polynomial.degreeLT.addLinearEquiv_apply, PeriodPair.summable_weierstrassPSummand, Submodule.fst_orthogonalDecomposition_apply, LinearEquiv.mem_dilatransvections_iff_finrank, Submodule.quotEquivOfEqBot_apply_mk, Submodule.smul_toAddSubmonoid, Submodule.comap_strictMono_of_surjective, Algebra.fg_trans, HilbertBasis.dense_span, Matrix.rank_eq_finrank_span_row, RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict, isSMulRegular_iff_torsionBy_eq_bot, Submodule.smul_starProjection_singleton, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, Submodule.toAddSubmonoid_sSup, LinearEquiv.ofSubmodules_symm_apply, Module.Basis.toDual_range, IsSemisimpleModule.exists_quotient_linearEquiv_submodule, LinearMap.kerComplementEquivRange_apply_coe, Submodule.mem_mul_span_singleton, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right, Submodule.mem_span_finset', Submodule.restrictScalarsEquiv_symm_apply, Submodule.mem_span_singleton_self, LinearMap.IsPerfectCompl.right_top_iff, finiteDimensional_vectorSpan_insert_set, LinearMap.quotientInfEquivSupQuotient_injective, Submodule.map₂_eq_span_image2, isSemisimpleModule_iff, isArtinian_of_submodule_of_artinian, Module.Basis.restrictScalars_repr_apply, Matrix.ker_toLin_eq_bot, ConvexCone.IsGenerating.top_le_span, Submodule.prod_span_singleton, ModuleCat.ker_eq_bot_of_mono, CliffordAlgebra.GradedAlgebra.ι_apply, Submodule.orthogonalFamily_self, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, LinearMapClass.ker_eq_bot, Submodule.smul_iSup, DirectSum.toBaseChange_bijective, Submodule.dualAnnihilator_sup_eq, LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, Finsupp.isCompl_range_lmapDomain_span, GradedTensorProduct.auxEquiv_mul, Submodule.IsMinimalPrimaryDecomposition.distinct, IsSelfAdjoint.dense_domain, TensorProduct.range_map_mono, Submodule.lTensorOne'_tmul, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, Module.End.submodule_pow_eq_zero_of_pow_eq_zero, RootPairing.CoPolarizationIn_eq, sSupIndep_isotypicComponents, Submodule.equivOpposite_apply, affineSpan_subset_span, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, Affine.Simplex.exradius_restrict, ClosedSubmodule.toSubmodule_iInf, Subrepresentation.mem_asSubmodule_iff, Submodule.rTensorOne'_tmul_one, Submodule.inner_orthogonalProjection_eq_of_mem_right, DirectSum.decompose_symm_algebraMap, LinearMap.ker_domRestrict, FractionalIdeal.coe_add, ContinuousMap.adjoin_id_eq_span_one_union, Submodule.isOrtho_iff_le, Ideal.Quotient.torsionBy_eq_span_singleton, Submodule.dualCoannihilator_sup_eq, Subbimodule.coe_mk, finiteDimensional_vectorSpan_singleton, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, MvPolynomial.homogeneousSubmodule_zero, Submodule.disjoint_ker_of_finrank_le, Ideal.Filtration.inf_submodule, Submodule.pi_top, LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal, QuotSMulTop.equivQuotTensor_naturality, Submodule.eq_factor_of_eq_factor_succ, Submodule.rTensorOne'_tmul, Submodule.isScalarTower', Submodule.finiteDimensional_inf_right, Submodule.toSubalgebra_mk, Finsupp.linearCombinationOn_range, Submodule.colon_span, HomogeneousLocalization.Away.span_mk_prod_pow_eq_top, LinearPMap.coe_smul, Submodule.coe_mem, TensorProduct.exists_finite_submodule_right_of_setFinite', realPart_comp_subtype_selfAdjoint, groupCohomology.π_comp_H0Iso_hom_assoc, ZSpan.coe_floor_self, Submodule.projective_units, RootPairing.algebraMap_rootFormIn, MvPolynomial.restrictSupport_mono, KaehlerDifferential.derivationQuotKerTotal_apply, AdicCompletion.transitionMap_comp_reduceModIdeal, LinearMap.ker_eq_bot', Submodule.map_subtype_embedding_eq, Submodule.le_linearEquiv_of_le_sSup, Module.jacobson_le_of_eq_bot, Submodule.sup_span_singleton_eq_top_iff, Module.jacobson_pi_eq_bot, eq_bot_of_generator_maximal_submoduleImage_eq_zero, MvPolynomial.mem_restrictDegree, Submodule.exists_dual_map_eq_bot_of_lt_top, ModuleCat.imageIsoRange_hom_subtype_assoc, Subalgebra.mul_toSubmodule_le, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, groupCohomology.mem_cocycles₂_iff, Submodule.LinearDisjoint.injective, AffineSubspace.direction_sup, Submodule.baseChange_eq_span, PointedCone.coe_lineal, Submodule.bot_pow, ZLattice.module_free, LinearMap.mem_submoduleImage, Submodule.dualCopairing_apply, Submodule.ClosedComplemented.isClosed_complement, LinearEquiv.toSpanNonzeroSingleton_apply, Affine.Simplex.orthogonalProjection_circumcenter, LinearMap.iterateKer_coe, Submodule.comap_snd, Submodule.mem_span_insert', Submodule.le_comap_mkQ, Ideal.coe_restrictScalars, Module.Flat.instSubalgebraToSubmodule, bot_isPrincipal, Submodule.fg_iSup, Submodule.neg_mem, Module.End.disjoint_genEigenspace, LinearMap.exact_smul_id_smul_top_mkQ, ContinuousLinearMap.coe_linearMap_equivRange, LinearPMap.map_zero, LinearMap.exists_ne_zero_of_sSup_eq, MvPolynomial.indicator_mem_restrictDegree, Submodule.coe_mapAlgEquiv_apply, MvPolynomial.coeffsIn_mul, iSupIndep.subtype_ne_bot_le_rank, IsSemisimpleModule.finite_tfae, FractionalIdeal.coe_inv_of_ne_zero, LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker, LinearPMap.map_add, LinearIndependent.notMem_span, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearIsometryEquiv.completeSpace_map, Submodule.localized₀_le_localized₀_of_smul_le, groupCohomology.H2π_comp_map_assoc, Submodule.disjoint_map, AdicCompletion.ofPowSMul_injective, HahnEmbedding.ArchimedeanStrata.nontrivial_stratum, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot, LinearPMap.domain_sSup, Submodule.ker_inclusion, AffineIndependent.finrank_vectorSpan_image_finset, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, Projectivization.submodule_injective, AffineSubspace.direction_iInf_of_mem, MvPolynomial.restrictSupport_zero, RootPairing.isCompl_rootSpan_ker_rootForm, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_liftK_hom, FractionalIdeal.isNoetherian_zero, groupHomology.mapCycles₂_comp_apply, DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top, Algebra.adjoin_toSubmodule_le, LinearIsometryEquiv.toSpanUnitSingleton_apply, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, Submodule.comap_subtype_eq_top, AffineSubspace.subtypeA_toAffineMap, LinearIndependent.span_repr_eq, Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, Submodule.inf_iSup_genEigenspace, norm_inner_eq_norm_tfae, LinearPMap.mkSpanSingleton'_apply, IsLocalization.coeSubmodule_le_coeSubmodule, Submodule.map_op_pow, RootPairing.rootForm_self_eq_zero_iff, RootPairing.corootSpan_mem_invtSubmodule_coreflection, Submodule.prodEquivOfIsCompl_symm_apply, Submodule.isCompl_orthogonal_of_hasOrthogonalProjection, Module.End.hasEigenvector_iff, Submodule.injective_tensorToSpan, Representation.linHom.invariantsEquivRepHom_apply, Submodule.Quotient.restrictScalarsEquiv_symm_mk, Submodule.projective_of_isUnit, PeriodPair.derivWeierstrassP_sub_coe, Module.Basis.restrictScalars_apply, RootPairing.invtRootSubmodule.eq_bot_iff, Submodule.toAddSubgroup_toIntSubmodule, instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent, Module.Basis.flag_succ, HasStrictFDerivAt.to_implicitFunction, Submodule.finite_quotient_smul, exteriorPower.ιMultiDual_apply_ιMulti, AffineSubspace.mk'_top, Profinite.NobelingProof.GoodProducts.span, Submodule.natAbs_det_equiv, MvPolynomial.le_coeffsIn_pow, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Module.Basis.mem_submodule_iff', Submodule.le_comap_map, Submodule.smithNormalFormBotBasis_def, Ideal.Filtration.Stable.exists_pow_smul_eq, Rep.resCoindHomEquiv_symm_apply, Module.End.IsFinitelySemisimple.restrict, Submodule.map_subtype_span_singleton, Matrix.range_toLin_eq_top, AdicCompletion.smul_mk, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, Submodule.instCovariantClassHSMulLe, Submodule.mapQ_eq_factor, AdicCompletion.exists_smodEq_pow_add_one_smul, Module.End.isFinitelySemisimple_iff, LinearPMap.adjointDomainMkCLM_apply, Submodule.closure_le, FractionalIdeal.coe_one, LinearPMap.mem_domain_iff, Submodule.mem_set_smul_of_mem_mem, MatrixModCat.mem_toModuleCatObj, set_has_minimal_iff_artinian, Submodule.starProjection_bot, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, linearIndependent_fin_succ', LinearIndepOn.notMem_span_of_insert, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, vectorSpan_mono, Valuation.ltSubmodule_monotone, LinearMap.injective_range_liftQ_of_exact, Submodule.fg_finset_sup, mem_skewAdjointMatricesLieSubalgebra, groupHomology.H2π_eq_iff, Submodule.span_eq, Submodule.mulRightMap_eq_mulMap_comp, Module.Grassmannian.finite_quotient, Submodule.le_isotypicComponent, Module.Presentation.cokernel_var, LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, ZLattice.covolume.tendsto_card_le_div', LinearMap.mem_range_self, IsNoetherian.wellFoundedGT, isNoetherian_submodule', QuadraticMap.IsometryEquiv.map_posDef_iff, Submodule.mem_inf, IsLocalizedModule.toLocalizedQuotient', exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, differentialIdeal_le_fractionalIdeal_iff, EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq, Submodule.span_set_smul, Submodule.comap_inf_map_of_injective, rank_span_finset_le, groupHomology.H1AddEquivOfIsTrivial_single, mem_span_insert_exchange, groupCohomology.mem_cocycles₁_iff, Module.End.disjoint_iInf_maxGenEigenspace, Ideal.quotientToQuotientRangePowQuotSucc_surjective, Affine.Simplex.direction_mongePlane, Submodule.coe_iInf, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, MvPolynomial.monomial_mem_coeffsIn, LinearMap.IsProj.top, Submodule.comap_covBy_of_surjective, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, Ideal.Filtration.submodule_span_single, Submodule.finrank_map_le, HahnEmbedding.Seed.coeff_baseEmbedding, finrank_span_eq_card, Ideal.Filtration.sup_N, Submodule.starProjection_unit_singleton, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, AddSubgroup.toZModSubmodule_symm, LinearIsometryEquiv.ofTop_apply, Submodule.prodComm_trans_prodEquivOfIsCompl, groupHomology.isoCycles₂_hom_comp_i_apply, LinearPMap.fst_apply, DirectSum.decompose_algebraMap, LinearMap.compLeftInverse_apply_of_bdd, Submodule.mul_smul_mul_eq_smul_mul_smul, RootPairing.IsRootSystem.span_root_eq_top, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, Submodule.sup_smul, AdicCompletion.pow_smul_top_eq_ker_eval, RootPairing.zero_le_posForm, Submodule.finrank_eq_zero, Module.length_bot, Submodule.quotientPi_apply, CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero, PowerBasis.mem_span_pow, Submodule.rTensorOne_tmul, Submodule.map_iInf, ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, Submodule.annihilator_top_inter_nonZeroDivisors, Rep.coinvariantsShortComplex_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, Module.End.restrict_eigenspace, Submodule.reflection_sub, Submodule.exists_fun_fin_finrank_span_eq, rTensor.inverse_of_rightInverse_comp_rTensor, EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, Module.Basis.flag_covBy, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, Submodule.range_lsum_smul, AffineSubspace.coe_vadd, Ideal.instIsTorsionFreeSubtypeMemSubmodule, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left, Module.Finite.of_isComplemented_domain, Polynomial.degreeLT.addLinearEquiv_apply', Submodule.singleton_smul, affineIndependent_iff_le_finrank_vectorSpan, Subspace.quotAnnihilatorEquiv_apply, skewAdjointPart_comp_subtype_selfAdjoint, groupCohomology.isoCocycles₁_inv_comp_iCocycles, Submodule.unitsToPic_apply, Submodule.toConvexCone_le_toConvexCone, Submodule.orderIsoMapComap_symm_apply', Affine.Simplex.circumcenter_restrict, Submodule.orderIsoMapComapOfBijective_symm_apply, LieSubmodule.sup_toSubmodule, Module.isTorsionBySet_iff_subseteq_ker_lsmul, Submodule.instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, Submodule.coe_zero, KaehlerDifferential.kerTotal_map, AffineMap.restrict.injective, Module.End.mem_genEigenspace_top, Submodule.coe_mulMap_comp_eq, Affine.Simplex.height_restrict, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, Submodule.prod_eq_top_iff, exteriorPower.oneEquiv_symm_apply, ModuleCat.imageIsoRange_inv_image_ι, Module.End.invtSubmodule.sup_mem, RingTheory.Sequence.isWeaklyRegular_append_iff', DirectSum.IsInternal.isCompl, instModuleFinite_of_discrete_submodule, Module.End.injOn_genEigenspace, RootPairing.isSimpleModule_weylGroupRootRep_iff, isNoetherian_quotient, LinearMap.finrank_range_le, Submodule.isIdempotentElemEquiv_apply_coe, Submodule.range_unitsToPic, Submodule.mem_toAddSubgroup, TensorProduct.exists_finite_submodule_left_of_finite', iSupIndep_iff_finset_sum_eq_imp_eq, LinearPMap.add_apply, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, IsSimpleModule.jacobson_eq_bot, LinearEquiv.submoduleMap_apply, Module.End.genEigenspace_one, ContinuousLinearEquiv.ofSubmodule'_apply, Submodule.spanSingleton_apply, Submodule.mem_of_span_top_of_smul_mem, Submodule.smul_le_right, Module.Flat.iff_lTensor_injective, LinearPMap.inverse_range, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, Ideal.Filtration.antitone, FractionalIdeal.coe_mul, LinearMap.range_eq_top, Module.Basis.mem_span_image, LieModule.Cohomology.mem_twoCocycle_iff, Rep.coindVEquiv_apply, Ideal.ker_tensorProductMk_quotient, Submodule.restrictScalars_mono, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, Submodule.exists_isInternal_prime_power_torsion_of_pid, TensorProduct.eq_zero_of_fg_of_subtype_eq_zero, PeriodPair.weierstrassP_add_coe, Algebra.inf_toSubmodule, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, Submodule.mem_span_mul_finite_of_mem_span_mul, Submodule.eq_bot_of_le_smul_of_le_jacobson_bot, Submodule.closure_subset_span, exteriorPower.map_comp_ιMulti, AffineSubspace.subtype_injective, groupCohomology.coboundariesOfIsCoboundary₁_coe, Module.End.isFinitelySemisimple_iff', span_selfAdjoint, VonNeumannAlgebra.IsIdempotentElem.mem_iff, AffineSubspace.subtype_linear, Submodule.FG.pow, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, Submodule.colon_eq_top_iff_subset, AddSubmonoid.toNatSubmodule_symm, AdicCompletion.val_apply_mem_smul_top_iff, PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice, Submodule.coe_inner, Subrepresentation.apply_mem_toSubmodule, FractionalIdeal.mul_def, DirectSum.decomposeLinearEquiv_apply_coe, Submodule.exists_smul_notMem_of_rank_lt, Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl, ZSpan.span_top, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, isSMulRegular_quotient_iff_mem_of_smul_mem, Submodule.IsLattice.span_eq_top, LinearMap.hasEigenvalue_zero_tfae, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, TensorProduct.exists_finite_submodule_of_finite, Algebra.adjoin_eq_span_of_subset, MeasureTheory.condExpL2_indicator_of_measurable, Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, RootPairing.iInf_ker_root'_eq, SchauderBasis.RankOneDecomposition.finrank_range, FractionalIdeal.coeSubmoduleHom_apply, derivationToSquareZeroEquivLift_symm_apply_apply_coe, GradedTensorProduct.mulHom_apply, Submodule.map_mul, rTensor.inverse_comp_rTensor, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite, Submodule.exists_mem_ne_zero_of_ne_bot, Submodule.closure_coe_iSup_map_single, MvPolynomial.mem_restrictSupport_iff, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, LinearMap.eqOn_span_iff, Submodule.linearEquiv_of_sSup_eq_top, MvPolynomial.degreesLE_zero, AddMonoidAlgebra.GradesBy.decompose_single, ContinuousMultilinearMap.codRestrict_apply_coe, AffineSubspace.topEquiv_symm_apply_coe, Submodule.coe_isComplEquivProj_apply, AffineSubspace.isometryEquivMap.coe_apply, Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal, Submodule.smul_mem_iff_of_isUnit, Module.Basis.flag_lt_flag, Subbimodule.coe_toSubbimoduleInt, IsCompactOperator.restrict, Submodule.prodEquivOfIsCompl_symm_apply_left, linearIndependent_fin_snoc, Submodule.sndL_comp_coe_orthogonalDecomposition, RootPairing.PolarizationIn_apply, Submodule.injective_subtype, Submodule.ker_mapQ, Submodule.rank_eq_spanRank_of_free, LinearIndepOn.mem_span_iff_id, Submodule.linearProjOfIsCompl_isCompl_projection, Submodule.le_traceDual, stereographic_neg_apply, LinearMap.mem_ker, Module.End.invtSubmodule.mk_eq_top_iff, LinearMap.liftQ₂_mk, Submodule.quotientEquivOfIsCompl_apply_mk_coe, Subalgebra.linearDisjoint_iff, InnerProductSpace.gramSchmidt_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, LinearEquiv.mem_dilatransvections_iff_rank_quotient, groupCohomology.coboundaries₂.coe_mk, IsFractional.pow, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, LinearMap.coe_domRestrict, Submodule.map_inr, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Submodule.localized'_eq_span, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap, Submodule.linearProjOfIsCompl_comp_subtype, Submodule.eq_top_of_isLocalized'_span, Module.End.injOn_maxGenEigenspace, IsFractionRing.coeSubmodule_le_coeSubmodule, Submodule.smul_top_eq_range_lsum, ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot, Submodule.torsionBySet_isInternal, Submodule.mem_span_finite_of_mem_span, Submodule.goursatFst_prod_goursatSnd_le, IsSemisimpleModule.sSup_simples_le, Submodule.comapMkQOrderEmbedding_eq, Representation.averageMap_invariant, Submodule.rank_eq_zero, PointedCone.gc_ofSubmodule_lineal, Submodule.IsLattice.finrank_of_pi, mem_fullyInvariantSubmodule_iff, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl, pinGroup.conjAct_smul_range_ι, Submodule.coe_subtypeₗᵢ, Submodule.sInf_orthogonal, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis, LinearMap.IsSymmetric.directSum_isInternal_of_commute, Submodule.IsCompl.projection_add_projection_eq_self, LinearMap.iInf_invariant, MvPolynomial.weightedHomogeneousComponent_directSum, IsSemisimpleModule.exists_simple_submodule, Submodule.smul_closure_subset, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, QuotSMulTop.map_exact, AddMonoidAlgebra.mem_grade_iff', ZSpan.exist_unique_vadd_mem_fundamentalDomain, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, Matrix.ker_toLin'_eq_bot_iff, Module.FaithfullyFlat.range_le_ker_of_exact_rTensor, LinearMap.quotKerEquivRange_symm_apply_image, Finsupp.restrictDom_comp_subtype, exists_subalgebra_of_fg, Module.Finite.span_singleton, Submodule.span_eq_iUnion_nat, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, rTensor_mkQ, Submodule.mul_toAddSubmonoid, Representation.coindMap_coe_apply_apply, Submodule.map_le_isotypicComponent, Collinear.finiteDimensional_vectorSpan, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, RingTheory.Sequence.isWeaklyRegular_append_iff, SchauderBasis.finrank_range_succSub_eq_one, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, IsArtinian.disjoint_partial_infs_eventually_top, exteriorPower.pairingDual_apply_apply_eq_one, groupCohomology.subtype_comp_d₀₁_assoc, Submodule.le_span_singleton_iff, LinearMap.range_coprod, Submodule.complete_of_finiteDimensional, Module.Flat.tensorProduct_mapIncl_injective_of_left, Submodule.mul_iSup, imaginaryPart_comp_subtype_selfAdjoint, Submodule.Quotient.equiv_symm_apply, iSupIndep.linearEquiv_apply, Submodule.pi_liftQ_eq_liftQ_pi, span_le_span_iff, EuclideanGeometry.Sphere.direction_orthRadius_le_iff, ZLattice.summable_norm_pow_inv, groupHomology.toCycles_comp_isoCycles₂_hom, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, HasRankNullity.rank_quotient_add_rank, groupCohomology.map_id_comp_H0Iso_hom, Submodule.FG.stabilizes_of_iSup_eq, Submodule.map_strict_mono_of_ker_inf_eq, Module.supportDim_quotSMulTop_succ_eq_supportDim, Submodule.convex, Module.Flat.iff_lTensor_injectiveₛ, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, SymmetricPower.range_mk, Submodule.coe_sub, Submodule.mem_smul_pointwise_iff_exists, Submodule.IsPrimary.radical_colon_singleton_eq_ite, Submodule.unitsQuotEquivRelPic_symm_apply, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, Submodule.torsionBy.mk_ideal_smul, Span.finsupp_linearCombination_repr, SetLike.algebraMap_mem_graded, Subalgebra.map_toSubmodule, Submodule.mem_span_iff_of_fintype, EuclideanGeometry.eq_or_eq_reflection_of_dist_eq, Affine.Simplex.incenter_restrict, LinearPMap.mem_graph_iff, Submodule.isClosed_orthogonal, Submodule.IsLattice.rank_of_pi, Module.jacobson_eq_bot_of_injective, mem_vectorSpan_pair_rev, Module.End.invtSubmodule.inf_mem, groupHomology.mapCycles₁_id_comp, IsModuleTopology.instQuot, SetLike.GradeZero.coe_algebraMap, AdicCompletion.ofPowSMul_val_apply_eq_zero, Submodule.span_sSup, Submodule.instCanonicallyOrderedAdd, InnerProductGeometry.angle_eq_angle_add_angle_iff, Submodule.comap_map_mkQ, Submodule.coe_torsionBySet, Submodule.mem_dualCoannihilator, Submodule.instFiniteQuotientIdealHSMulTop, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, Submodule.tmul_mem_baseChange_of_mem, Submodule.norm_orthogonalProjection_apply, Submodule.orderIsoMapComap_symm_apply, Submodule.neg_bot, toENat_rank_span_set, Submodule.iSup_eq_span, CliffordAlgebra.reverse_mem_evenOdd_iff, LieModule.Cohomology.add_apply_apply, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Submodule.torsionBySet_torsionBySet_eq_top, LinearMap.singularValues_pos_iff_lt_finrank_range, IsSemisimpleModule.jacobson_le_ker, MeasureTheory.condExpL1CLM_lpMeas, Submodule.rTensorOne_tmul_one, Submodule.toLinearMap_prodEquivOfIsCompl_symm, LinearEquiv.fixedReduce_eq_smul_iff, LinearMap.IsIdempotentElem.comp_eq_left_iff, Submodule.le_of_isLocalized_span, PeriodPair.latticeBasis_one, Subbimodule.coe_toSubbimoduleNat, ClosedSubmodule.mem_orthogonal_toSubmodule_iff, Submodule.finrank_eq_rank, Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge, ZLattice.covolume_eq_det_mul_measureReal, Submodule.ker_liftQ_eq_bot, LinearPMap.map_neg, RootPairing.iInf_ker_coroot'_eq, Subspace.finrank_add_finrank_dualCoannihilator_eq, DirectSum.IsInternal.toBaseChange_bijective, MvPolynomial.mem_weightedHomogeneousSubmodule, Submodule.le_traceDual_comm, Submodule.mem_span_singleton_mul, multiple_mem_span_of_mem_localization_span, groupCohomology.cocyclesOfIsMulCocycle₂_coe, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, span_lt_top_of_card_lt_finrank, Submodule.span_iUnion, Function.Exact.linearMap_rangeRestrict, PeriodPair.weierstrassP_sub_coe, Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule, Module.IsTorsionBySet.quotient, Ideal.primaryComponent_map_mem, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, Module.Finite.range, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective, Submodule.Quotient.instSmallQuotient, LieSubmodule.sSup_toSubmodule, Submodule.span_range_natDegree_eq_adjoin, Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left, LinearIndependent.linearCombinationEquiv_symm_apply, Submodule.equivSubtypeMap_apply, Submodule.biSup_comap_eq_top_of_range_eq_biSup, Submodule.ClosedComplemented.isClosed, ZSpan.isAddFundamentalDomain, Submodule.IsMinimalPrimaryDecomposition.injOn, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, Submodule.isIdempotentElemEquiv_symm_apply_coe, Submodule.inf_orthogonal, AddSubgroup.coe_toZModSubmodule, mem_skewAdjointMatricesSubmodule, MvPolynomial.mem_coeffsIn, FiniteDimensional.finiteDimensional_submodule, abs_signedDist_eq_dist_iff_vsub_mem_span, Module.Relations.Solution.isPresentation_iff, AffineSubspace.direction_iInf, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, Submodule.map_eq_bot_iff, Submodule.Quotient.nontrivial_of_ne_top, Submodule.IsOrtho.le, ArchimedeanClass.ball_top, Submodule.IsLasker.exists_isMinimalPrimaryDecomposition, IsLinearTopology.hasBasis_submodule', Finsupp.disjoint_supported_supported, VonNeumannAlgebra.IsStarProjection.mem_iff, Submodule.coe_inf, NumberField.Units.instDiscrete_unitLattice, LinearMap.IsSymmetric.direct_sum_isInternal, Submodule.det_reflection, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, LinearPMap.map_sub, LinearMap.quotKerEquivRange_apply_mk, Submodule.disjoint_def', Submodule.sum_mem_biSup, Submodule.mem_of_isLocalized_span, Matrix.ker_diagonal_toLin', DividedPowerAlgebra.submodule_span_prod_dp_eq_top, FractionalIdeal.isPrincipal_inv, rank_span_le, FractionalIdeal.coeToSet_coeToSubmodule, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, Submodule.neg_iInf, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, ClosedSubmodule.mem_sup, Ideal.toCotangent_apply, Submodule.inner_orthogonalProjection_eq_of_mem_left, Submodule.IsMinimalPrimaryDecomposition.minimal, LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate, rank_submodule_eq_one_iff, Module.End.mem_iInf_maxGenEigenspace_iff, TensorProduct.spanFinrank_top_le_of_fg, groupHomology.isoCycles₁_hom_comp_i_apply, Submodule.starConvex, ClosedSubmodule.toSubmodule_injective, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, LinearMap.range_prod_le, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, Submodule.orderIsoMapComap_apply, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, Submodule.topologicalClosure_mono, AffineSubspace.subtypeₐᵢ_linear, ZLattice.exists_forall_abs_repr_le_norm, linearIndependent_fin_succ, AffineMap.restrict.coe_apply, ClosedSubmodule.mem_iSup, Submodule.linearMap_eq_iff_of_eq_span, Ideal.Filtration.bot_N, Submodule.empty_set_smul, CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom, Submodule.isPrimary_decomposition_pairwise_ne_radical, RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, Submodule.one_eq_span_one_set, Polynomial.span_of_finite_le_degreeLT, IsIntegralClosure.range_le_span_dualBasis, ModuleCat.imageIsoRange_inv_image_ι_assoc, IsSemisimpleModule.sSup_simples_eq_top, Submodule.bot_colon', groupCohomology.H1π_eq_zero_iff, AddMonoidAlgebra.single_mem_grade, PeriodPair.hasSum_weierstrassP, Submodule.mem_right_iff_eq_zero_of_disjoint, Submodule.toAddSubgroup_strictMono, DirectSum.IsInternal.subordinateOrthonormalBasis_def, PeriodPair.coeff_weierstrassPSeries, Algebra.Extension.h1Cotangentι_ext_iff, PeriodPair.isOpen_compl_lattice_diff, Finsupp.linearCombination_range, exteriorPower.ιMulti_family_span_of_span, NumberField.fractionalIdeal_rank, GradedAlgHom.coe_mk', LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace, Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, Ideal.Filtration.pow_smul_le_pow_smul, LinearMap.finrank_range_adjoint, MvPolynomial.decomposition.decompose'_apply, MvPolynomial.restrictSupport_nsmul, LinearIndependent.span_eq_top_of_card_eq_finrank, groupCohomology.coboundaries₁.val_eq_coe, Submodule.fg_of_linearEquiv, PeriodPair.derivWeierstrassP_coe, maximal_orthonormal_iff_orthogonalComplement_eq_bot, Submodule.restrictScalars_sup, Submodule.mulRightMap_apply, MvPolynomial.mem_degreesLE, Module.Finite.instIsCoatomicSubmodule, AdicCompletion.pow_smul_top_le_ker_eval, Module.Basis.SmithNormalForm.le_ker_coord_of_notMem_range, LieHom.quotKerEquivRange_invFun, Module.isTorsionBy_iff_mem_ker_lsmul, Submodule.top_le_span_range_iff_forall_exists_fun, LieSubalgebra.toSubmodule_eq_bot, Submodule.IsLattice.free, LinearPMap.map_smul, Module.injOn_dualMap_subtype_span_range_range, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, mem_affineSpan_iff_exists, Submodule.map₂_le, LieSubalgebra.coe_ofLe, Algebra.iInf_toSubmodule, isSimpleModule_iff, LinearMap.eventually_isCompl_ker_pow_range_pow, fourierSubalgebra_coe, Submodule.isOrtho_top_right, Submodule.isOpenMap_mkQ, Submodule.singleton_set_smul, Real.Convex.dimH_eq_finrank_vectorSpan, Submodule.nontrivial_span_singleton, Submodule.linearDisjoint_op, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, Submodule.quotientEquivOfIsCompl_symm_apply, Polynomial.aeval_apply_smul_mem_of_le_comap', Submodule.spanRank_toENat_eq_iInf_finset_card, Submodule.exists_smith_normal_form_of_rank_eq, MvPolynomial.monomial_mem_restrictSupport, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, GradedTensorProduct.auxEquiv_tmul, Module.End.eventually_disjoint_ker_pow_range_pow, ModuleCat.kernelIsoKer_hom_ker_subtype, exteriorPower.map_injective_field, monotone_stabilizes_iff_noetherian, ContinuousLinearMap.ker_prod, Submodule.subset_span_finite_of_subset_span, Submodule.topologicalClosure_mem_invtSubmodule, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, Submodule.fst_map_fst, groupHomology.H1ToTensorOfIsTrivial_H1π_single, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, Algebra.Extension.H1Cotangent.val_add, Submodule.map_surjective_of_surjective, LinearEquiv.coe_ofEq_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply, coord_norm', RootPairing.algebraMap_posRootForm_posForm, DirectSum.IsInternal.collectedOrthonormalBasis_mem, LinearMap.ker_eq_bot_of_cancel, LinearMap.eqOn_sup, Submodule.coe_torsionBy, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Submodule.dualAnnihilator_gc, Ideal.quotientToQuotientRangePowQuotSucc_injective, groupCohomology.cocyclesMk₁_eq, Submodule.add_mem_sup, Profinite.NobelingProof.spanFinBasis.span, RootPairing.span_root'_eq_top, Submodule.range_powSMulQuotInclusion, DirectSum.decomposeLinearEquiv_apply, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, Subalgebra.finiteDimensional_toSubmodule, Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection, Submodule.gc_map_comap, exteriorPower.alternatingMapLinearEquiv_comp, collinear_iff_rank_le_one, Finsupp.linearCombination_restrict, Ideal.stableFiltration_N, Algebra.Extension.H1Cotangent.val_smul, AffineSubspace.direction_top, Submodule.mem_projectivization_iff_submodule_le, Submodule.instCovariantClassHSMulLe_1, Submodule.finiteQuotientOfFreeOfRankEq, LinearPMap.dExt_iff, Submodule.neg_eq_self, Module.eval_ker, MvPolynomial.mem_homogeneousSubmodule, ContinuousLinearMap.HasLeftInverse.isClosed_complement, Submodule.map_op_mul, Module.finite_def, Submodule.topologicalClosure_coe, Submodule.finite_ne_bot_of_iSupIndep, Submodule.smul_mem_iff', groupHomology.cyclesOfIsCycle₁_coe, LinearEquiv.ofSubmodule'_toLinearMap, finrank_top, DirectSum.decomposeLinearEquiv_symm_comp_lof, exteriorPower.basis_coord, Submodule.sup_dualAnnihilator_le_inf, linearIndepOn_union_iff, Subalgebra.toSubmodule_toSubalgebra, Submodule.inf_comap_le_comap_add, FractionalIdeal.mem_span_mul_finite_of_mem_mul, ClosedSubmodule.mem_orthogonal_iff, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, LinearIndependent.repr_range, range_deriv_subset_closure_span_image, AddMonoidHom.coe_toIntLinearMap_ker, ZLattice.covolume.tendsto_card_div_pow', LocallyConstant.ker_comapₗ, IsSemisimpleModule.exists_end_ringEquiv, Module.End.mem_eigenspace_iff, Module.isPrincipal_submodule_iff, TensorProduct.map₂_mk_top_top_eq_top, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, Function.Exact.iff_linearMap_rangeRestrict, Module.isTorsionBySet_annihilator_top, LinearPMap.supSpanSingleton_apply_smul_self, RootPairing.range_polarizationIn, Submodule.pow_mem_pow, RootPairing.restrictScalars_coe_root, Submodule.supIndep_torsionBy, Submodule.mem_span_range_iff_exists_fun, exteriorPower.presentation_relation, Algebra.adjoin_union_coe_submodule, Subspace.dualAnnihilator_iInf_eq, mem_selfAdjointMatricesSubmodule, Submodule.mulMap_one_left_eq, groupHomology.d₂₁_apply_mem_cycles₁, stereographic_target, TensorProduct.quotTensorEquivQuotSMul_symm_mk, Submodule.iSup_map_single, LinearMap.range_le_iff_comap, Submodule.starProjection_apply_mem, Submodule.coe_set_mk, Submodule.cardQuot_eq_one_iff, LinearMap.IsIdempotentElem.range_mem_invtSubmodule, LieModule.Cohomology.smul_apply_apply, Submodule.mem_sSup_of_mem, Submodule.toAddSubmonoid_le, groupCohomology.coboundariesToCocycles₂_apply, LinearPMap.inverse_apply_eq, EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Submodule.restrictScalars_injective, AddMonoidAlgebra.gradeBy.gradedMonoid, Submodule.smul_sup, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite, Submodule.quotDualCoannihilatorToDual_injective, Affine.Simplex.centroid_restrict, MultilinearMap.codRestrict_apply_coe, Finsupp.supported_empty, Submodule.quotientPi_symm_apply, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, Submodule.FG.mul, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, Module.Flat.flat_iff_torsion_eq_bot_of_isBezout, Module.AEval.mem_mapSubmodule_symm_apply, Submodule.dfinsuppSum_mem, Valuation.ltSubmodule_le_leSubmodule, Module.jacobson_quotient_of_le, GradedAlgebra.coe_algebraMap_apply, ClosedSubmodule.toSubmodule_sSup, Submodule.mem_toAddSubmonoid, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, LinearPMap.coprod_apply, DirectSum.toBaseChange_injective, TensorProduct.exists_finite_submodule_of_setFinite', groupCohomology.H2π_eq_zero_iff, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, Submodule.liftQ_apply, LinearIsometryEquiv.submoduleMap_symm_apply_coe, LinearMap.disjoint_ker_iff_injOn, LieSubalgebra.disjoint_toSubmodule, LieModule.Cohomology.instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, LinearPMap.domain_sup, Subspace.dualRestrict_surjective, KaehlerDifferential.kerTotal_mkQ_single_mul, Coplanar.finiteDimensional_vectorSpan, groupCohomology.mapCocycles₁_comp_i_assoc, PointedCone.coe_ofConeComb, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', groupCohomology.cocycles₁.val_eq_coe, Submodule.torsionBy_isTorsion_nonZeroDivisor, Module.Basis.flag_wcovBy, Module.Baer.extensionOfMax_to_submodule_eq_top, Submodule.le_orthogonal_iff_le_orthogonal, AddSubgroup.coe_toIntSubmodule, Submodule.ker_subtypeL, Submodule.bot_mul, LinearMap.kerComplementEquivRange_symm_apply, LinearPMap.supSpanSingleton_apply_self, Polynomial.Chebyshev.T_iterate_derivative_mem_span_T, Submodule.mem_orthogonal, groupCohomology.H1π_comp_map_apply, Submodule.torsionBySet_le_torsionBySet_pow, StrongDual.mem_polarSubmodule, ClassGroup.equivPic_symm_apply, LinearMap.lift_rank_range_add_rank_ker, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, Submodule.mulMap_comm_of_commute, groupCohomology.cocycles₁_map_one, fg_adjoin_of_finite, Submodule.fst_map_snd, TensorAlgebra.GradedAlgebra.ι_apply, Ideal.restrictScalars_mul, Submodule.lt_map_of_comap_lt_of_surjective, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, Submodule.map_inf, Submodule.Quotient.isCentralScalar, PeriodPair.latticeEquiv_symm_apply, HahnEmbedding.ArchimedeanStrata.isInternal_stratum', Submodule.mker_spanSingleton, AdicCompletion.val_add, Absorbent.submodule_eq_top, Submodule.IsLocalizedModule.localized'FrameHom_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, Submodule.comap_lt_of_lt_map_of_injective, exteriorPower.instFinite, AffineSubspace.direction_lt_of_nonempty, FractionalIdeal.den_mul_self_eq_num, Submodule.disjoint_span_singleton_of_notMem, ClosedSubmodule.toSubmodule_le_toSubmodule, Submodule.isQuotientEquivQuotientPrime_iff, Submodule.map_smul', EuclideanGeometry.orthogonalProjection_mem, span_eq_top_of_isLocalizedModule, LieSubmodule.sInf_toSubmodule_eq_iInf, LinearEquiv.coord_self, Submodule.le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot, Submodule.isCentralScalar, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, exteriorPower.alternatingMapToDual_apply_ιMulti, groupCohomology.π_comp_H2Iso_hom_assoc, Submodule.quotientPi_aux.map_add, Affine.Simplex.orthogonalProjectionSpan_restrict, Module.Presentation.cokernel_G, Submodule.nonempty, Submodule.annihilator_span, isArtinian_submodule', Representation.Coinvariants.mk_eq_zero, isClosed_nullSubmodule, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, Algebra.adjoin_eq_span, Submodule.nat_power_gradedMonoid, LinearEquiv.ofEq_symm, IsSemisimpleModule.exists_end_algEquiv, TensorProduct.spanFinrank_top_eq_of_residueField, groupHomology.mem_cycles₁_of_mem_boundaries₁, Submodule.isCompl_iff_disjoint, Submodule.IsCompl.projection_apply_eq_zero_iff, Module.supportDim_le_supportDim_quotSMulTop_succ, QuotSMulTop.equivQuotTensor_naturality_mk, Module.exists_isPrincipal_quotient_of_finite, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, Submodule.span_union, Submodule.mulMap_eq_mul'_comp_mapIncl, DirectSum.decomposeLinearEquiv_symm_apply, Submodule.existsUnique_from_graph, Submodule.one_smul, LinearEquiv.ofLeftInverse_apply, DirectSum.decompose_bracket, CliffordAlgebra.even_toSubmodule, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.range_smul', span_fourierLp_closure_eq_top, weightedVSub_mem_vectorSpan, Module.finrank_eq_spanFinrank_of_free, Module.End.genEigenspace_zero_nat, Algebra.toSubmodule_eq_top, Representation.le_comap_invariants, LinearMap.exact_map_mkQ_range, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, LieSubmodule.coe_lieSpan_submodule_eq_iff, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Submodule.small_iSup, Finsupp.disjoint_lsingle_lsingle, Affine.Simplex.setInterior_restrict, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, AdicCompletion.val_one, Submodule.eq_iSup_inf_genEigenspace, AffineSubspace.finiteDimensional_sup, IsLocalization.smul_mem_iff, WithCStarModule.map_top_submodule, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Submodule.mkQ_map_self, LinearIndepOn.mem_span_iff, AddMonoidAlgebra.mem_grade_iff, Submodule.rank_add_le_rank_add_rank, RootPairing.RootPositiveForm.isSymm_posForm, FractionalIdeal.isNoetherian_iff, Submodule.sup_mul, Submodule.mem_smul_top_iff, SubmodulesRingBasis.leftMul, ZLattice.covolume.tendsto_card_le_div, Module.support_quotSMulTop, Module.End.mem_invtSubmodule_symm_iff_le_map, Module.equiv_free_prod_directSum, DirectSum.decomposeAlgEquiv_apply, Submodule.torsionBySet_span_singleton_eq, AffineIndependent.finrank_vectorSpan, Submodule.smul_one_eq_span, Finsupp.codisjoint_supported_supported_iff, CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range, AddMonoidAlgebra.grade.decompose_single, Submodule.mem_span_image_finset_iff_exists_fun, Submodule.spanRank_sup_le_sum_spanRank, Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot, Submodule.IsCompl.projection_apply, Submodule.smul_assoc, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat, Module.Basis.self_mem_flag_iff, Submodule.add_mem_iff_left, LinearMap.comp_codRestrict, InnerProductSpace.mem_span_gramSchmidt, Submodule.mulLeftMap_eq_mulMap_comp, Submodule.span_smul, Representation.subrepresentation_apply, Module.End.genEigenspace_top, Submodule.map_pointwise_smul, Submodule.map_zero, groupHomology.mapCycles₂_hom, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, MeasureTheory.integrable_condExpL2_indicator, Module.End.invtSubmodule.isCompl_mk_iff, AdicCompletion.factor_eval_liftRingHom, rank_quotient_add_rank_le, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, LinearMap.mem_selfAdjointSubmodule, groupHomology.isoCycles₂_inv_comp_iCycles_apply, ImplicitFunctionData.range_rightDeriv, CStarAlgebra.span_nonneg_inter_closedBall, LinearMap.finrank_range_dualMap_eq_finrank_range, Subbimodule.coe_toSubmodule, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, Affine.Simplex.excenterWeights_restrict, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Submodule.sub_mem_orthogonal_of_inner_right, AffineEquiv.ofEq_symm, Ideal.decomposition_erase_inf, Submodule.nontrivial_iff_ne_bot, Submodule.iSup_torsionBy_eq_torsionBy_prod, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, Submodule.toLocalizedQuotient'_mk, LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, vectorSpan_singleton, Submodule.image_span_subset, LinearIndepOn.notMem_span_iff_id, Algebra.Extension.Hom.subToKer_apply_coe, Ideal.Filtration.Stable.exists_forall_le, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, Submodule.toSubMulAction_strictMono, Submodule.reflection_eq_self_iff, LinearMap.map_le_range, stereographic_source, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self, ZLattice.summable_norm_sub_rpow, Rep.indCoindIso_hom_hom_toLinearMap, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum', LinearMap.IsProj.eq_conj_prod_map', LinearMap.ker_zero, Subalgebra.pi_toSubsemiring, IsIntegral.mem_span_pow, AffineMap.restrict.linear_aux, LinearEquiv.submoduleMap_symm_apply, Submodule.IsHomogeneous.mem_iff, GradedAlgHom.toGradedRingHom_injective, FractionalIdeal.coe_sup, MvPolynomial.mem_restrictDegree_iff_sup, LinearMap.map_codRestrict, Submodule.set_smul_le_of_le_le, LinearMap.eventually_iInf_range_pow_eq, Submodule.mem_span_pair, RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule, ZLattice.abs_repr_lt_of_norm_lt, Submodule.set_smul_eq_iSup, EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, Submodule.Quotient.mk_surjective, LinearMap.mem_range, ContinuousLinearMap.isClosed_eigenspace, MonoidAlgebra.supportedEquivFinsupp_apply_apply, groupHomology.cyclesMk₂_eq, LinearMap.BilinForm.finrank_orthogonal, RingFilterBasis.SubmodulesBasis.inter, mem_nullSubmodule_iff, DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_eq, Module.fgSystem.instIsDirectedOrderSubtypeSubmoduleFG, mem_span_of_iInf_ker_le_ker, ContinuousMultilinearMap.codRestrict_toMultilinearMap, Polynomial.degreeLT.addLinearEquiv_symm_apply', Submodule.map_inl, Submodule.finrank_add_inf_finrank_orthogonal', LieSubmodule.sSup_toSubmodule_eq_iSup, Submodule.LinearDisjoint.rank_le_one_of_flat_of_self, ContinuousLinearMap.projKerOfRightInverse_comp_inv, TensorProduct.eq_of_fg_of_subtype_eq, LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul, IsZLattice.span_top, KaehlerDifferential.kerTotal_mkQ_single_smul, Module.Basis.self_mem_span_image, Submodule.instInvertibleSubtypeMemVal, AffineSubspace.linear_equivMapOfInjective, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, Submodule.topologicalAddGroup_quotient, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, Subbimodule.coe_toSubmodule', groupHomology.H1π_eq_zero_iff, Submodule.disjoint_iff_add_eq_zero, DirectSum.IsInternal.toBaseChange_injective, Ideal.mem_iInf_smul_pow_eq_bot_iff, Submodule.zero_mem, LinearMap.fixedSubmodule_comp_inf_fixedSubmodule_le, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', LinearMap.BilinForm.IsSymm.restrict, groupHomology.π_comp_H1Iso_hom_assoc, Affine.Simplex.median_restrict, Ideal.Filtration.pow_smul_le, Hausdorffification.lift_comp_of, LinearMap.trace_eq_sum_trace_restrict, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, ClosedSubmodule.mem_sSup, RootPairing.root'_apply_apply_mem_of_mem_span, LinearMap.disjoint_ker_of_nondegenerate_restrict, Polynomial.sup_ker_aeval_le_ker_aeval_mul, Finsupp.supported_mono, Submodule.toIsOrderedCancelAddMonoid, Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint, NonUnitalAlgebra.toSubmodule_eq_top, isNoetherian_of_fg_of_noetherian, Submodule.topologicalClosure_eq_top_iff, Module.End.span_orbit_mem_invtSubmodule, LinearMap.range_liftBaseChange, groupHomology.H2π_comp_map, SubmodulesRingBasis.inter, RootPairing.rootSpanMem_reflectionPerm_self, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, groupHomology.mem_cycles₂_of_mem_boundaries₂, Submodule.coe_smul, Subspace.dualEquivDual_def, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, Submodule.coe_span_eq_span_of_surjective, Ring.map_jacobson_le, groupCohomology.cocycles₂.val_eq_coe, affineSpan_coe_preimage_eq_top, Submodule.mem_one, TensorProduct.quotientTensorEquiv_apply_tmul_mk, Module.FinitePresentation.out, Submodule.QuotientTorsion.instIsTorsionFree, Submodule.exists_finset_span_eq_linearIndepOn, exteriorPower.zeroEquiv_ιMulti, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, smul_vsub_rev_mem_vectorSpan_pair, MvPolynomial.ker_evalₗ, LinearPMap.mem_graph_iff', Submodule.Quotient.isScalarTower, LinearMap.range_comp_le_range, AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul, Submodule.reflection_bot, LinearMap.surjective_comp_linearProjOfIsCompl, LinearMap.exact_subtype_ker_map, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, IsSemisimpleModule.isCoatomic_submodule, Module.End.invtSubmodule.codisjoint_iff, Ideal.smul_restrictScalars, Valuation.ltSubmodule_v_le_of_mem, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_fst, Algebra.Extension.H1Cotangent.map_apply_coe, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, PeriodPair.analyticOnNhd_derivWeierstrassP, Polynomial.eval_eq_sum_degreeLTEquiv, Submodule.mulMap'_surjective, MvPowerSeries.coe_hasEvalIdeal, Submodule.subtypeL_apply, AddMonoidHom.coe_toIntLinearMap_map, AffineSubspace.coe_direction_eq_vsub_set_left, Submodule.finrank_span_eq_finrank_span, Submodule.restrictScalars_mem, Submodule.ClosedComplemented.isCompl_complement, Submodule.map_unop_one, Module.isTorsionBySet_quotient_iff, Submodule.mem_orthogonalBilin_iff, Submodule.mem_smul_span, Submodule.span_zero_singleton, groupHomology.H1π_comp_map_assoc, Subspace.dualLift_rightInverse, Representation.Coinvariants.mk_eq_iff, Ideal.natAbs_det_equiv, ZSpan.quotientEquiv.symm_apply, LinearMap.map_coe_ker, OrthogonalFamily.range_linearIsometry, Submodule.torsion_gc, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, Submodule.IsPrincipal.generator_mem, Submodule.finrank_map_subtype_eq, groupHomology.instEpiModuleCatH1π, Submodule.coe_dualAnnihilator_span, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_apply_ker, Submodule.ker_orthogonalProjection, NumberField.mem_span_integralBasis, IsLocalRing.span_eq_top_of_tmul_eq_basis, Affine.Simplex.closedInterior_restrict, ClosedSubmodule.mem_mk, GradedAlgHom.map_mem, Submodule.sup_orthogonal_of_hasOrthogonalProjection, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, Submodule.mem_carrier, groupCohomology.isoCocycles₂_inv_comp_iCocycles, MeasureTheory.lpTrimToLpMeas_ae_eq, LinearMap.ofIsCompl_add, AffineSubspace.direction_sInf, Submodule.apply_mem_span_image_of_mem_span, AdicCompletion.transitionMap_map_pow, LinearEquiv.ofSubmodule'_apply, Submodule.starProjection_orthogonalComplement_singleton_eq_zero, Submodule.isOrtho_iSup_right, Submodule.FG.directedSystem, HahnEmbedding.Partial.mem_domain, span_lt_of_subset_of_card_lt_finrank, Submodule.mem_span_of_mem, Submodule.IsOrtho.disjoint, LinearMap.IsIdempotentElem.isCompl, Submodule.powSMulQuotInclusion_mk, EuclideanGeometry.orthogonalProjection_orthogonalProjection, exteriorPower.map_injective, rank_quotient_le, vectorSpan_add_self, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self, Submodule.map_lt_map_iff_of_injective, Submodule.neg_eq_self_iff_neg_le, Submodule.iSup_smul, MvPolynomial.mem_coeffsIn_iff_coeffs_subset, Submodule.mem_iSup_finset_iff_exists_sum, groupCohomology.δ₀_apply, Submodule.eq_top_iff_forall_basis_mem, EuclideanGeometry.orthogonalProjection_vsub_mem_direction, exteriorPower.basis_repr_apply, Submodule.iSup_eq_span', Representation.invtSubmodule.top_mem, LinearIndependent.repr_eq, IsAssociatedPrime.annihilator_le, Submodule.HasOrthogonalProjection.exists_orthogonal, Submodule.mk_quotientEquivOfIsCompl_apply, Submodule.smul_mem_iff, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, MvPolynomial.weightedDecomposition.decompose'_eq, Submodule.starProjection_top, Submodule.prodEquivOfIsCompl_symm_apply_right, Submodule.coe_mapIic_apply, le_sigNeg_of_negDef, Submodule.submoduleOf_eq_top, Subspace.dualCopairing_nondegenerate, HahnEmbedding.Seed.mem_domain_baseEmbedding, exteriorPower.presentation_R, Submodule.iInf_orthogonal, Submodule.map_liftQ, Submodule.piQuotientLift_single, Submodule.restrictScalars.isScalarTower, Submodule.mem_span, Ideal.FinrankQuotientMap.span_eq_top, Submodule.pow_eq_span_pow_set, finiteDimensional_direction_affineSpan_image_of_finite, CliffordAlgebra.submodule_map_mul_reverse, groupHomology.instEpiModuleCatH2π, ContinuousLinearEquiv.submoduleMap_symm_apply, NumberField.mem_span_basisOfFractionalIdeal, Submodule.exists_isInternal_prime_power_torsion, LinearIndepOn.image_subset_span_image_extend, Submodule.mul_smul, AddMonoidHom.coe_toIntLinearMap_range, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, Subbimodule.coe_baseChange, LinearMap.BilinForm.mem_orthogonal_iff, Polynomial.mem_ker_modByMonic, mem_vectorSpan_pair, Submodule.torsionBy_one, Module.rank_le_one_iff_top_isPrincipal, Submodule.dualAnnihilator_top, Subalgebra.coe_pi, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, PointedCone.ofSubmodule_iSup, Submodule.eq_span_singleton_of_surjective, Submodule.instIsOrderedRing, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero, AffineSubspace.topEquiv_apply, Submodule.liftQSpanSingleton_apply, LinearEquiv.ofTop_symm_apply, Submodule.exists_isCompl, LinearMap.comap_eq_sup_ker_of_disjoint, Finsupp.mem_span_range_iff_exists_finsupp, groupCohomology.cocyclesMk₂_eq, Submodule.Quotient.mk_neg, LinearIsometry.completeSpace_map, AddMonoidAlgebra.supported_mono, GradedTensorProduct.tmul_coe_mul_zero_coe_tmul, Affine.Simplex.mongePoint_restrict, rank_span_of_finset, Rep.indCoindIso_inv_hom_toLinearMap, Submodule.span_mono, Module.End.eigenspace_le_maxGenEigenspace, Submodule.coe_smul_of_tower, PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, Ideal.pi_mkQ_rTensor, MvPolynomial.coeffsIn_eq_span_monomial, Module.Dual.exists_forall_mem_ne_zero_of_forall_exists, Submodule.finrank_mono, Submodule.range_map_nonempty, Submodule.mulLeftMap_apply_single, ModuleCat.disjoint_span_sum, ConvexCone.IsGenerating.span_eq_top, Finsupp.single_mem_span_single, ContinuousLinearMap.IsIdempotentElem.commute_iff, KaehlerDifferential.quotKerTotalEquiv_symm_apply, ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, LinearMap.quotKerEquivOfSurjective_symm_apply, Submodule.mapQ_mkQ, EuclideanGeometry.hasFDerivAt_inversion, mem_coeSubmodule_conductor, AffineSubspace.direction_iInf_of_mem_iInf, Submodule.finite_finset_sup, CliffordAlgebra.evenOdd_mul_le, mem_isotypicComponents_iff, LinearIndependent.repr_ker, Submodule.comap_surjective_of_injective, LinearMap.ker_prod, AffineSubspace.direction_sInf_of_mem, Submodule.top_le_span_of_exact_of_retraction, Submodule.factorPow_comp_powSMulQuotInclusion, groupHomology.H1π_comp_map, Affine.Simplex.eulerPoint_restrict, Submodule.finrank_add_le_finrank_add_finrank, groupHomology.d₃₂_apply_mem_cycles₂, Pi.dim_spanSubset, Submodule.toLinearPMap_apply_aux, MvPolynomial.coeffsIn_pow, LieSubmodule.mk_eq_bot_iff, Ideal.Filtration.mono, OrthonormalBasis.span_apply, Module.End.generalized_eigenvec_disjoint_range_ker, Submodule.le_div_iff, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, rTensor.inverse_apply, Submodule.span_sSup', Submodule.mulMap_map_comp_eq, AdicCompletion.val_sub, IsHausdorff.eq_iff_smodEq, Submodule.mem_span_triple, MeasureTheory.Measure.addHaar_submodule, Submodule.cardQuot_bot, GradedTensorProduct.comm_coe_tmul_coe, Submodule.mem_torsionBy_iff, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, Module.Basis.sumQuot_inr, Module.Basis.flag_le_iff, instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe, QuadraticMap.restrict_apply, LinearPMap.closure_def, IsSimpleModule.span_singleton_eq_top, Module.Flat.iff_lift_lsmul_comp_subtype_injective, ContinuousMap.adjoin_id_eq_span_one_add, ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe, AffineSubspace.coe_inclusion_apply, Submodule.quotientPi_aux.left_inv, Ideal.range_finsuppTotal, Submodule.lt_sup_iff_notMem, Set.Mapsto.mem_invtSubmodule, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, Module.length_eq_coheight, Affine.Simplex.ExcenterExists.touchpoint_restrict, AffineSubspace.signedInfDist_singleton, groupHomology.boundariesOfIsBoundary₂_coe, PointedCone.ofSubmodule_inf, LinearMap.IsProj.submodule_eq_bot_iff, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Module.Finite.top, LinearPMap.mem_domain_of_mem_graph, Submodule.finrank_le_one_iff_isPrincipal, groupHomology.cyclesMk₁_eq, Submodule.ne_bot_iff, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem, Module.End.isNilpotent_restrict_sub_algebraMap, Ideal.primaryComponent_mem, instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian, Submodule.FG.lTensor.directLimit_apply, Submodule.prod_bot, RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial, LieSubmodule.coe_toSubmodule, Submodule.finrank_span_eq_finrank, Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf, LinearMap.IsProj.codRestrict_ker, Collinear.finrank_le_one, AffineSubspace.vadd_mem_iff_mem_direction, Module.fgSystem.equiv_comp_of, FractionalIdeal.mul_def', Submodule.map_iSup_comap_of_surjective, AddMonoidAlgebra.grade.isInternal, groupHomology.mapCycles₂_comp_i_assoc, RootPairing.posRootForm_posForm_nondegenerate, Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply, isLinearTopology_iff_hasBasis_open_submodule, ArchimedeanClass.mem_closedBall_iff, Affine.Simplex.excenterWeightsUnnorm_restrict, groupCohomology.isoCocycles₁_hom_comp_i, LinearMap.singularValues_finrank_range_self, Submodule.range_inclusion, Module.Flat.instSubtypeMemSubmoduleSubmoduleAlgebra, MvPolynomial.HomogeneousSubmodule.gradedMonoid, ContinuousLinearMap.projKerOfRightInverse_apply_idem, Submodule.mem_traceDual, Submodule.spanFinrank_top, RootPairing.coe_bot, Submodule.coe_iSup_of_directed, LinearMap.comap_prod_prod, Submodule.mapHom_id, LinearMap.domRestrict₂_apply, AffineSubspace.subtypeₐᵢ_linearIsometry, Submodule.comap_le_comap_iff_of_surjective, Module.End.invtSubmodule.top_mem, Submodule.map_mono, LinearMap.IsIdempotentElem.mem_range_iff, IsPrecomplete.prec, Submodule.mul_subset_mul, AdicCompletion.val_neg, Module.Basis.eq_bot_of_rank_eq_zero, Submodule.mem_span_image_finset_iff_exists_fun', Submodule.set_smul_bot, Module.End.mem_genEigenspace_one, PeriodPair.hasSumLocallyUniformly_aux, NonUnitalAlgebra.inf_toSubmodule, LieSubalgebra.toSubmodule_eq_top, LinearMap.IsProj.trace, IsLocalRing.CotangentSpace.map_eq_top_iff, Submodule.smul_comap_le_comap_smul, LinearPMap.mem_graph, Submodule.zero_eq_bot, AffineSubspace.direction_bot, Submodule.map_iInf_comap_of_surjective, Subspace.map_le_dualAnnihilator_dualAnnihilator, rank_range_of_injective, HahnEmbedding.ArchimedeanStrata.archimedean_stratum, LinearMap.span_singleton_inf_orthogonal_eq_bot, Module.isTorsionBy_quotient_iff, Submodule.basisOfPid_bot, Submodule.factor_comp_apply, MvPolynomial.restrictSupport_add, exists_maximal_linearIndepOn, Submodule.span_singleton_eq_one_iff, Subalgebra.adjoin_eq_span_of_eq_span, EuclideanGeometry.Sphere.IsTangent.isTangentAt, Submodule.AddMonoidHom.coe_toIntLinearMap_comap, groupCohomology.mapCocycles₁_comp_i_apply, LinearMap.BilinForm.orthogonal_top_eq_ker, ContinuousLinearMap.coe_codRestrict_apply, ZLattice.isAddFundamentalDomain, LinearMap.isClosed_or_dense_ker, Submodule.IsLattice.sup, Submodule.complementedLattice, Submodule.quotEquivOfEq_mk, Submodule.isInternal_prime_power_torsion, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', LinearMap.restrict_smul_one, Submodule.annihilator_top, Module.End.mapsTo_maxGenEigenspace_of_comm, groupHomology.mapCycles₂_id_comp_apply, Submodule.image2_subset_map₂, Submodule.coe_eq_zero, Submodule.coe_closure, LinearMap.range_domRestrict, AffineSubspace.sup_direction_le, Polynomial.det_taylorLinearEquiv, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, Submodule.instIsTorsionFree, groupCohomology.cocycles₂_ext_iff, LinearMap.continuous_domRestrict, Submodule.IsPrimary.inf, LinearEquiv.mem_stabilizer_fixedSubmodule, Algebra.Extension.h1Cotangentι_apply, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, Submodule.coe_subtype, Submodule.mulMap_comp_lTensor, LinearEquiv.rank_map_eq, isNoetherian_span_of_finite, LinearMap.isCoatom_ker_of_surjective, Submodule.mem_sInf, RootPairing.algebraMap_coroot'In_apply, Module.End.independent_maxGenEigenspace, Submodule.smul_torsionBy, AdicCompletion.transitionMap_ideal_mk, Submodule.map₂_sup_left, Submodule.coe_neg, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, LinearMap.linearEquiv_of_ne_zero, LinearMap.BilinForm.le_orthogonal_orthogonal, LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker, Submodule.smul_le, Submodule.mem_localized₀, LinearPMap.adjointDomainMkCLMExtend_apply, Submodule.sup_eq_top_iff, dimH_orthogonalProjection_le, LinearMap.ker_sup_ker_le_ker_comp_of_commute, LinearMap.range_ofIsCompl, GradedLieAlgebra.toGradedBracket, RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic, Submodule.traceDual_bot, instDiscreteTopologySubtypeMemSubmoduleIntComap, Module.End.mem_maxGenEigenspace, Submodule.torsionBy_isTorsionBy, Module.Basis.flag_le_flag, AdicCompletion.transitionMap_map_mul, EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq, Module.End.genEigenspace_div, Submodule.add_mem_iff_right, Submodule.span_span, Module.Finite.iff_fg, groupHomology.H2π_comp_map_apply, Submodule.mem_iSup_of_mem, Submodule.adjoint_orthogonalProjection, Submodule.lTensorOne_symm_apply, LinearMap.tensorEqLocus_tmul, exteriorPower.map_comp_ιMulti_family, Submodule.mul_eq_map₂, MvPolynomial.mul_monomial_mem_coeffsIn, EuclideanGeometry.reflection_apply', Submodule.mul_le, Submodule.fg_top, AffineIsometryEquiv.ofEq_rfl, LinearMap.iterateRange_coe, RootPairing.rootFormIn_self_smul_coroot, Submodule.le_orthogonalBilin_orthogonalBilin, Profinite.NobelingProof.GoodProducts.span_iff_products, Submodule.tensorToSpan_apply_tmul, Submodule.isOrtho_bot_right, ClosedSubmodule.toSubmodule_bot, ZLattice.le_norm_of_le_abs_repr, exteriorPower.map_id, IsPrecomplete.prec', LinearMap.ofIsCompl_left_apply, EuclideanGeometry.oangle_self_orthogonalProjection, LinearMap.eqLocus_eq_top, Submodule.isCompl_comap_subtype_of_isCompl_of_le, le_isotypicComponent_iff, TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_apply_tmul, LinearMap.IsProj.submodule_eq_top_iff, Submodule.mk_le_mk, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, Ideal.ofList_cons_smul, Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule, LinearMap.ker_le_iff, LieModule.Cohomology.twoCochain_val_apply, Module.Finite.of_fg, HahnEmbedding.Seed.hahnCoeff_apply, CliffordAlgebra.iSup_ι_range_eq_top, LinearIsometry.strictConvexSpace_range_iff, linearIndependent_iff_notMem_span, Submodule.iInf_colon, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, Function.Exact.linearEquivOfSurjective_apply, Submodule.mem_orthogonal_singleton_iff_inner_left, groupCohomology.coboundaries₁_ext_iff, Submodule.fg_iff_finiteDimensional, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, iSupIndep_iff_dfinsupp_lsum_injective, span_flip_eq_top_iff_linearIndependent, Module.End.eigenspace_mem_invtSubmodule, Submodule.map_strict_mono_or_ker_sup_lt_ker_sup, Submodule.mem_adjoint_iff, LinearMap.le_comap_isotypicComponent, Submodule.CoFG.top, MvPolynomial.weightedHomogeneousComponent_mem, Submodule.span_biUnion, Submodule.eq_top_of_localization₀_maximal, Finsupp.supportedEquivFinsupp_symm_apply_coe, Submodule.span_singleton_eq_range, CliffordAlgebra.submodule_comap_pow_reverse, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, LinearEquiv.toSpanNonzeroSingleton_one, Submodule.lTensorOne'_one_tmul, LinearMap.compAlternatingMap_codRestrict, Module.Basis.self_mem_flag, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K, LinearMap.mem_graph_iff, LinearMap.coe_quotientInfToSupQuotient, Submodule.range_dualMap_mkQ_eq, MatrixModCat.toModuleCat_map, Polynomial.toMatrix_sylvesterMap, TensorProduct.exists_finite_submodule_right_of_finite, LinearMap.subtype_compMultilinearMap_codRestrict, Finsupp.supportedEquivFinsupp_apply_support_val, LinearIsometryEquiv.reflections_generate_dim, GradedAlgebra.proj_apply, Ideal.coe_piOrderIso_symm_apply, Polynomial.coeff_divByMonic_mem_pow_natDegree_mul, FractionalIdeal.mem_coe, Submodule.orthogonal_le, RootPairing.isIrreducible_iff_invtRootSubmodule, exists_mem_ne_zero_of_rank_pos, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection, Submodule.IsCompl.projection_eq_self_sub_projection, AffineEquiv.coe_ofEq_apply, AffineSubspace.direction_inf_of_mem_inf, ClosedSubmodule.toSubmodule_inf, finiteDimensional_bot, ContinuousLinearMap.exist_extension_of_finiteDimensional_range, LieSubmodule.codisjoint_toSubmodule, LieModule.maxGenEigenSpace_toEnd_eq_top, Submodule.span_inter, FractionalIdeal.coeToSubmodule_injective, Submodule.smul_le_of_le_smul_of_le_jacobson_bot, Module.length_ne_top_iff_finiteDimensionalOrder, LieSubalgebra.inf_toSubmodule, groupCohomology.π_comp_H2Iso_hom_apply, LinearPMap.mkSpanSingleton_apply, PeriodPair.hasSum_weierstrassPExcept, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, is_simple_module_of_finrank_eq_one, Module.Basis.flag_le_ker_coord_iff, Submodule.toAddSubgroup_eq_top, Submodule.small_span, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant, Submodule.coe_span_eq_self, Algebra.Generators.H1Cotangent.δ_eq_δAux, CliffordAlgebra.even.lift.aux_apply, isPathConnected_compl_of_isPathConnected_compl_zero, AffineSubspace.mem_direction_iff_eq_vsub_right, LinearMap.IsProj.bot, Submodule.norm_coe, Submodule.exists_lieSubalgebra_coe_eq_iff, Submodule.finrank_add_finrank_orthogonal, instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents, AffineMap.restrict.linear, Hausdorffification.lift_of, Submodule.isTorsionFree_iff_torsion_eq_bot, eventuallyConst_of_isNoetherian, ZLattice.summable_norm_sub_zpow, Submodule.iInf_colon_iUnion, Submodule.orthogonal_eq_top_iff, Submodule.comap_unop_pow, Module.End.ker_aeval_ring_hom'_unit_polynomial, Submodule.map_subtype_top, Submodule.pow_eq_npowRec, AddSubmonoid.coe_toNatSubmodule, Submodule.mem_toConvexCone, exteriorPower.pairingDual_apply_apply_eq_one_zero, Submodule.lipschitzWith_orthogonalProjection, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, Submodule.map_sup_comap_of_surjective, LinearMap.BilinForm.orthogonal_bot, TopModuleCat.kerι_apply, QuotSMulTop.map_comp, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Submodule.coe_copy, Submodule.exists_fg_le_subset_range_rTensor_inclusion, Submodule.one_mul, LieSubmodule.iSup_toSubmodule_eq_top, Module.End.mem_invtSubmodule_adjoint_iff, Module.End.genEigenspace_nat, Module.ker_algebraMap_end, orthogonalFamily_iff_pairwise, Submodule.span_span_coe_preimage, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, Submodule.torsionBySet_univ, Representation.mem_coindV, AffineSubspace.coe_subtype, Representation.coind_apply, groupHomology.isoCycles₁_hom_comp_i_assoc, ContinuousLinearEquiv.submoduleMap_apply, Submodule.inf_orthogonal_eq_bot, FractionalIdeal.abs_det_basis_change, Submodule.ClosedComplemented.exists_submodule_equiv_prod, Submodule.mul_top_eq_top_of_mul_eq_one, span_range_eq_top_iff_surjective_finsuppLinearCombination, LinearMap.map_span_le, Submodule.isOrtho_sSup_left, Submodule.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul, IsAdicComplete.StrictMono.factorPow_comp_extend, Rep.invariantsFunctor_map_hom, Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq, finrank_span_singleton, LieAlgebra.mem_corootSpace', MonoidAlgebra.mem_supported, RootPairing.rootSpan_mem_invtSubmodule_reflection, Affine.Simplex.orthogonalProjectionSpan_reindex, Subalgebra.coe_toSubmodule, LinearPMap.vadd_apply, LinearMap.le_eqLocus, Submodule.span_sup, LinearMap.ker_eq_bot_of_injective, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, Submodule.FG.jacobson_smul_lt, Module.Finite.map, Submodule.rank_le_one_iff_isPrincipal, SModEq.top, LinearMap.range_dualMap_le_dualAnnihilator_ker, subalgebra_top_finrank_eq_submodule_top_finrank, Submodule.span_singleton_mul, bot_lt_isotypicComponents, stereographic_apply, MeasureTheory.inner_condExpL2_eq_inner_fun, Submodule.mem_stabilizer_submodule_iff_map_eq, Submodule.finite_dualAnnihilator_iff, Submodule.fg_iff_compact, Submodule.linearProjOfIsCompl_comp_bijective_of_exact, Representation.quotient_apply, RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff, MeasureTheory.mem_lpMeas_self, eq_bot_of_generator_maximal_map_eq_zero, Finsupp.supported_iUnion, groupCohomology.π_comp_H1Iso_hom_apply, LinearMap.continuous_iff_isClosed_ker, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, Submodule.exists_of_finrank_lt, IsCoercive.ker_eq_bot, Submodule.neg_inf, ContinuousLinearMap.ker_prod_ker_le_ker_coprod, LinearMap.rTensor_range, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Representation.Coinvariants.mem_ker_of_eq, LinearIsometry.strictConvexSpace_range, LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, TensorProduct.exists_finite_submodule_right_of_finite', OrthogonalFamily.independent, IsLocalRing.CotangentSpace.span_image_eq_top_iff, AlternatingMap.codRestrict_apply_coe, isPrecomplete_iff, LinearEquiv.coord_apply_smul, LinearPMap.ext_iff, Submodule.topologicalAddGroup, Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo, AddSubgroup.toIntSubmodule_toAddSubgroup, RootPairing.restrictScalars_toLinearMap_apply_apply, LinearMap.finrank_maxGenEigenspace_zero_eq, Module.End.genEigenspace_le_maximal, Submodule.CoFG.sInf, Submodule.fstL_comp_coe_orthogonalDecomposition, RootPairing.finrank_corootSpan_eq, Submodule.restrictScalars_iSup, isPathConnected_compl_of_one_lt_codim, LinearMap.ofIsCompl_right_apply, Submodule.map_pow, Submodule.mem_span_set', Polynomial.sylvesterMap_apply_coe, LinearMap.BilinForm.orthogonal_le, LinearMap.coprod_map_prod, monotone_stabilizes_iff_artinian, Submodule.vaddCommClass, Polynomial.degreeLT.addLinearEquiv_natAdd, Units.submodule_isFractional, linearDepOn_iffₛ, LinearMap.ker_le_ker_comp, riesz_extension, linearIndepOn_union_iff_quotient, Submodule.starProjection_minimal, PeriodPair.differentiableOn_weierstrassPExcept, RootPairing.coe_top, EuclideanGeometry.orthogonalProjection_linear, Valuation.mem_ltSubmodule_iff, ContinuousLinearEquiv.ofSubmodule'_symm_apply, pinGroup.involute_act_ι_mem_range_ι, iSupIndep_of_dfinsupp_lsum_injective, Module.End.mem_genEigenspace_nat, Submodule.inclusion_injective, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, Submodule.le_comap_single_pi, Submodule.mulMap_comp_map_inclusion, ContinuousLinearMap.completeSpace_ker, Submodule.orthogonalProjection_orthogonal_apply_eq_zero, AffineSubspace.signedInfDist_def, FiniteArchimedeanClass.submodule_strictAnti, Submodule.spanFinrank_eq_zero_iff_eq_bot, PeriodPair.derivWeierstrassPExcept_add_coe, IsSimpleModule.toIsSimpleOrder, LinearMap.submoduleComap_surjective_of_surjective, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, Submodule.starProjection_mem_subspace_eq_self, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, exteriorPower.basis_repr, Submodule.angle_coe, Module.AEval.annihilator_top_eq_ker_aeval, NumberField.Units.unitLattice_rank, LinearMap.mem_fixedSubmodule_iff, Submodule.ker_mkQ, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, Subspace.dualAnnihilator_le_dualAnnihilator_iff, Submodule.finrank_le, instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents, groupHomology.π_comp_H2Iso_hom_apply, Submodule.LinearDisjoint.one_right, isArtinian_sup, Submodule.lTensorOne_tmul, LinearEquiv.fixedReduce_mk, instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId, Submodule.coe_pi, Submodule.quotientPiLift_mk, LinearMap.fixedSubmodule_inf_fixedSubmodule_le_comp, LinearIndepOn.notMem_span_iff, Module.Relations.Solution.span_relation_le_ker_π, Submodule.continuousSMul_quotient, LinearMap.range_eq_map, PeriodPair.differentiableOn_weierstrassP, Submodule.mem_colon_singleton, Module.Flat.iff_rTensor_injectiveₛ, UnitAddTorus.span_mFourier_closure_eq_top, Submodule.LinearDisjoint.val_mulMap_tmul, Submodule.FG.span, Submodule.mkQ_surjective, Module.Baer.ExtensionOf.le, Submodule.pow_subset_pow, LinearMap.trace_restrict_eq_of_forall_mem, Module.End.isSemisimple_iff', Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, Module.Dual.finrank_ker_add_one_of_ne_zero, Module.Finite.bot, LinearEquiv.reduce_mk, exteriorPower.alternatingMapLinearEquiv_symm_apply, LinearIndependent.notMem_span_image, isLinearTopology_iff_hasBasis_submodule, IsAdicComplete.mk_lift, Submodule.finrank_quotient_eq_sum, wellFoundedGT, Ideal.primaryComponent.map_ker_eq, ZLattice.normBound_spec, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, DirectSum.IsInternal.submodule_iSup_eq_top, Submodule.top_smul, groupHomology.mapCycles₁_hom, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, AdicCompletion.factor_evalₐ_eq_eval, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, Submodule.mem_iSup_of_chain, MvPolynomial.homogeneousSubmodule_one_pow, Subalgebra.restrictScalars_toSubmodule, Submodule.mem_map_of_mem, ContinuousLinearMap.HasLeftInverse.isCompl_complement, LinearMap.exists_extend, isNoetherian_submodule_left, AffineSubspace.mem_mk', Submodule.orderIsoMapComapOfBijective_apply, groupHomology.isoCycles₁_inv_comp_iCycles, Function.Exact.linearEquivOfSurjective_symm_apply, Submodule.le_dualAnnihilator_iff_le_dualCoannihilator, Submodule.smul_mem_span_smul', affineIndependent_iff_finrank_vectorSpan_eq, GradedAlgHom.comp_toGradedRingHom, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, StarAlgebra.adjoin_eq_span, IsArtinian.isSemisimpleModule_iff_jacobson, Submodule.span_smul_eq, Submodule.orthogonalProjectionFn_eq, Polynomial.span_le_degreeLE_of_finite, Submodule.span_eq_top_of_ne_zero, Submodule.mem_iSup_iff_exists_finset, ZSpan.discreteTopology_pi_basisFun, QuadraticMap.lift_mk, Submodule.mul_eq_span_mul_set, Submodule.IsOrtho.ge, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, Module.length_quotient, RootPairing.finrank_rootSpanIn, Module.length_eq_height, Affine.Simplex.signedInfDist_affineCombination, Ideal.cotangentEquivIdeal_symm_apply, Module.flat_iff, Submodule.mem_colon, LinearMap.ker_id_sub_eq_of_proj, Polynomial.taylorLinearEquiv_symm, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, Submodule.spanFinrank_bot, Submodule.bot_orthogonal_eq_top, Submodule.valFromGraph_mem, FractionalIdeal.val_eq_coe, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, TensorProduct.map_ker, Submodule.coe_toNonUnitalSubalgebra, Submodule.span_empty, EuclideanGeometry.angle_self_orthogonalProjection, Submodule.exists_fg_le_eq_rTensor_subtype, groupHomology.single_mem_cycles₁_of_mem_invariants, LieSubalgebra.mem_mk_iff', FractionalIdeal.isNoetherian, QuadraticMap.radical_le_ker_polarBilin, groupHomology.coe_mapCycles₁, NumberField.Units.logEmbeddingEquiv_apply, ZLattice.covolume.tendsto_card_le_div'', Submodule.localized₀_iSup, groupHomology.toCycles_comp_isoCycles₁_hom, Module.End.isNilpotent_restrict_of_le, Submodule.map_orthogonal, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, Submodule.iSup_eq_toSubmodule_range, TensorProduct.exists_finite_submodule_of_setFinite, Submodule.smul_span, TensorProduct.exists_finite_submodule_left_of_setFinite', RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff, exteriorPower.map_apply_ιMulti, Submodule.CoFG.inf, MvPolynomial.one_coeffsIn, LinearMap.ker_eq_bot_iff_range_eq_top, Submodule.map_iInf_of_ker_le, isSimpleModule_iff_isCoatom, LinearMap.iSup_range_single_le_iInf_ker_proj, NumberField.basisOfFractionalIdeal_apply, PeriodPair.hasSum_sumInvPow, ContinuousAlternatingMap.codRestrict_apply_coe, AddMonoidAlgebra.mem_supported', Module.Basis.ofZLatticeComap_repr_apply, iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero, signedDist_eq_dist_iff_vsub_mem_span, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, LieSubalgebra.coe_lieSpan_submodule_eq_iff, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, TensorProduct.rTensor_injective_of_forall_fg_rTensor_injective, Submodule.mulExact_unitsMap_spanSingleton_unitsToPic, AffineSubspace.angle_coe, LinearMap.finrank_eq_of_isPerfPair, QuotSMulTop.map_apply_mk, LinearMap.ker_restrict, RootPairing.posRootForm_posForm_anisotropic, Submodule.mem_sSup_iff_exists_finset, Submodule.dualAnnihilator_bot, Module.Basis.mem_toFlag, LinearPMap.le_graph_of_le, LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute, LinearMap.disjoint_single_single, AddMonoidAlgebra.mem_span_support', QuadraticMap.IsometryEquiv.map_negDef_iff, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, Submodule.spanRank_eq_zero_iff_eq_bot, LinearMap.eventually_codisjoint_ker_pow_range_pow, Submodule.sup_toAddSubmonoid, Submodule.mem_finsetInf, groupHomology.mapCycles₂_comp_i_apply, AdicCompletion.eval_of, MonoidAlgebra.supported_mono, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, rank_quotient_add_rank_of_divisionRing, Submodule.setSemiring_smul_def, Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff, Module.End.isNilpotent_restrict_genEigenspace_top, EuclideanGeometry.orthogonalProjection_eq_self_iff, linearIndepOn_insert, groupCohomology.cocyclesIso₀_hom_comp_f_apply, LinearMap.map_eq_top_iff, Submodule.instNontrivial, groupHomology.boundariesToCycles₂_apply, Module.Finite.span_finset, Submodule.quotientPi_aux.right_inv, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1, groupCohomology.subtype_comp_d₀₁, AddMonoidAlgebra.decomposeAux_single, EuclideanGeometry.reflection_subtype, Submodule.subset_span, PeriodPair.periodic_weierstrassP, Submodule.orthogonal_le_orthogonal_iff, LinearPMap.mem_domain_iff_of_eq_graph, Submodule.map_range_rTensor_subtype_lid, Submodule.orthogonal_le_iff_orthogonal_le, Submodule.span_singleton_le_iff_mem, Submodule.isOpen_mono, groupHomology.cyclesOfIsCycle₂_coe, LinearMap.det_eq_det_mul_det, isNoetherian_sup, LinearMap.BilinForm.orthogonal_eq_top_iff, Submodule.map_comap_le, FiniteDimensional.instSubtypeMemSubmoduleMap, isSMulRegular_on_quot_iff_lsmul_comap_eq, Submodule.eq_zero_of_bot_submodule, QuadraticMap.nondegenerate_iff_radical_eq_bot, ContinuousLinearEquiv.coord_norm', LinearEquiv.coe_ofTop_symm_apply, Ideal.coe_torsionOf, Submodule.IsLattice.finite, Submodule.mem_sup, groupHomology.isoCycles₂_hom_comp_i, IsFractional.nsmul, LinearMap.injective_domRestrict_iff, IsIntegral.fg_adjoin_singleton, Module.map_eval_injective, groupHomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, LinearMap.support_singularValues, LinearMap.mem_span_iff_bound, Submodule.mapHom_apply, Submodule.fstEquiv_symm_apply_coe, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, Submodule.coe_set_smul, Submodule.snd_orthogonalDecomposition_apply, groupHomology.isoCycles₂_inv_comp_iCycles, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal, asymptoticCone_submodule, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, Module.Basis.ofZLatticeBasis_repr_apply, groupHomology.mkH1OfIsTrivial_apply, tendsto_card_div_pow_atTop_volume', CliffordAlgebra.ι_mem_evenOdd_one, IsLocalization.span_invSubmonoid, LinearMap.isCompl_span_singleton_orthogonal, FractionalIdeal.spanSingleton_def, fromModuleCatToModuleCatLinearEquiv_apply, FiniteArchimedeanClass.ball_strictAnti, Module.Finite.span_of_finite, OrzechProperty.injective_of_surjective_of_submodule', LinearPMap.domRestrict_domain, Submodule.notMem_of_ortho, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, Submodule.top_coe, Submodule.torsionBy_le_torsionBy_of_dvd, IsIsotypic.linearEquiv_finsupp, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, Submodule.isCompact_of_fg, fromModuleCatToModuleCatLinearEquiv_symm_apply_coe, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, LinearMap.surjective_rangeRestrict, AffineSubspace.isometryEquivMap.apply_symm_apply, Submodule.coe_torsion_eq_annihilator_ne_bot, Submodule.starProjection_le_starProjection_iff, RootPairing.span_root_image_eq_top_of_forall_orthogonal, AffineSubspace.inclusion_rfl, IsSemisimpleModule.eq_bot_or_exists_simple_le, Submodule.linearProjOfIsCompl_range, Submodule.disjoint_def, IsLocalization.coeSubmodule_strictMono, PiTensorProduct.span_tprod_eq_top, finrank_eq_one_iff_of_nonzero, set_has_maximal_iff_noetherian, Module.End.ker_pow_le_ker_pow_finrank, Module.End.iSup_maxGenEigenspace_eq_top, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, Submodule.Quotient.subsingleton_iff, Submodule.span_preimage_le, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Submodule.equivOpposite_symm_apply, Submodule.toBaseChange_surjective', isAssociatedPrime_iff, Submodule.eq_bot_iff, Submodule.instOrthogonalCompleteSpace, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, groupCohomology.coboundaries₁_le_cocycles₁, LinearMap.restrict_coe_apply, linearIndependent_option', LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, Submodule.Quotient.smulCommClass, linearIndepOn_id_insert, Submodule.restrictScalars_iInf, Submodule.instIsModularLattice, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, ClosedSubmodule.coe_iSup, Submodule.coe_mapAlgHom_apply, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, Submodule.finite_iSup, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, Ideal.isPrimary_decomposition_pairwise_ne_radical, Submodule.range_ker_disjoint, Submodule.le_traceDual_mul_iff, FractionalIdeal.equivNum_apply, Submodule.cardQuot_top, Submodule.restrictScalars_eq_top_iff, Submodule.exists_mem_sup, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, Finsupp.lsingle_range_le_ker_lapply, LinearMap.BilinForm.orthogonal_top_eq_bot, Submodule.finsuppSum_mem, AddSubgroup.relIndex_eq_natAbs_det, isNoetherian_of_submodule_of_noetherian, Submodule.coe_norm, Submodule.orthogonalDecomposition_apply, Submodule.isOrtho_self, MvPolynomial.range_mapAlgHom, Submodule.span_singleton_smul_le, Submodule.span_insert, Submodule.smul_mem_smul, IsArtinian.set_has_minimal, groupHomology.single_one_mem_boundaries₁, Module.Grassmannian.projective_quotient, Submodule.instSMulCommClass_1, Submodule.map_comap_subtype, Submodule.span_range_subtype_eq_top_iff, Submodule.spanRank_top, AntilipschitzWith.completeSpace_range_clm, Submodule.isCompl_span_singleton_of_isCoatom_of_notMem, IsLocalizedModule.smul_mem_finsetIntegerMultiple_span, LinearMap.isCompl_of_proj, LinearIsometry.isComplete_map_iff', ClosedSubmodule.toSubmodule_top, Finsupp.mem_span_image_iff_linearCombination, ModuleCat.mono_iff_ker_eq_bot, Submodule.baseChange_top, Module.Flat.top_mul_submoduleAlgebra, AdicCompletion.val_zero, Submodule.le_map_of_comap_le_of_surjective, Submodule.comap_unop_one, exteriorPower.map_comp, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice, Submodule.FG.sup, Module.Basis.toFlag_carrier, instIsAtomisticSubmodule, Module.End.isNilpotent.restrict, groupHomology.π_comp_H1Iso_inv_apply, Rep.mkQ_hom_toFun, lift_rank_range_le, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, ZSpan.vadd_mem_fundamentalDomain, Submodule.fg_bot, exteriorPower.ιMultiDual_apply_nondiag, LinearMap.codRestrict_apply, sSup_simples_eq_top_iff_isSemisimpleModule, Polynomial.taylor_mem_degreeLT, Subrepresentation.mem_ofSubmodule_iff, AddMonoidAlgebra.decomposeAux_eq_decompose, Submodule.exists_dual_map_eq_bot_of_notMem, Submodule.span_monotone, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, LinearMap.separatingLeft_iff_ker_eq_bot, exteriorPower.presentation_var, Submodule.finset_span_isCompactElement, GradedTensorProduct.tmul_algebraMap_mul_coe_tmul, ZSpan.fract_apply, groupCohomology.isoCocycles₂_hom_comp_i_apply, LinearIsometryEquiv.ofEq_rfl, LieAlgebra.mem_corootSpace, Submodule.map_le_iff_le_comap, Matrix.range_diagonal, Submodule.mulMap_op, LinearEquiv.ofEq_rfl, AdicCompletion.mk_apply_coe, Submodule.torsionBySet.mk_smul, LinearMap.BilinForm.Nondegenerate.ker_eq_bot, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, Module.End.genEigenspace_restrict_eq_top, AffineSubspace.vsub_right_mem_direction_iff_mem, isNoetherian_top_iff, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, HahnEmbedding.Partial.sSupFun_strictMono, Submodule.Quotient.norm_mk_le, Module.map_jacobson_le, MeasureTheory.lpMeasToLpTrim_ae_eq, Submodule.orthogonal_eq_inter, Submodule.FG.small, MeasureTheory.eLpNorm_condExpL2_le, Submodule.mem_sSup_of_directed, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute, smul_vsub_mem_vectorSpan_pair, Submodule.isPathConnected, finrank_vectorSpan_range_add_one_le, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, Module.Flat.tensorProduct_mapIncl_injective_of_right, ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe, Submodule.mem_span_set_iff_exists_finsupp_le_finrank, ContinuousLinearEquiv.coord_self, UniformOnFun.continuousSMul_submodule_of_image_bounded, IsLocalRing.map_mkQ_eq_top, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, LinearMap.linearProjOfIsCompl_of_proj, LinearMap.ofIsCompl_subtype_zero_eq, Subbimodule.smul_mem, Submodule.one_le, LinearMap.trace_eq_sum_trace_restrict', LinearEquiv.finrank_map_eq, LinearEquiv.toLinearMap_ofTop, Submodule.map_covBy_of_injective, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, Submodule.map_subtype_range_inclusion, finrank_bot, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, Submodule.eq_top_of_localization_maximal, ContinuousLinearEquiv.coord_norm, Submodule.existsUnique_add_of_isCompl, FiniteDimensional.subalgebra_toSubmodule, exteriorPower.map_surjective, LieSubmodule.toSubmodule_eq_top, AddSubgroup.toIntSubmodule_closure, MeasureTheory.lpMeasToLpTrim_smul, Module.End.invtSubmodule.zero, groupCohomology.coboundaries₂_ext_iff, NonUnitalSubalgebra.mem_toSubmodule, PointedCone.mem_ofSubmodule_iff, isStarProjection_iff_eq_starProjection, MvPolynomial.C_mem_coeffsIn, Submodule.torsionBySet_ideal_isTorsion_of_noZeroDivisors, LinearPMap.mem_adjoint_domain_iff, Module.Basis.coe_mkFinCons, IsLocalization.mem_coeSubmodule, Submodule.ker_inr, LinearMap.IsSymmetricProjection.le_iff_range_le_range, vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan, RootPairing.rootSpan_eq_top_iff, CliffordAlgebra.GradedAlgebra.lift_ι_eq, OrderIso.setIsotypicComponents_symm_apply, AddSubgroup.mem_toZModSubmodule, Submodule.linearProjOfIsCompl_ker, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, groupCohomology.cocyclesOfIsCocycle₂_coe, LinearEquiv.lift_rank_map_eq, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, LinearMap.not_hasEigenvalue_zero_tfae, EuclideanGeometry.orthogonalProjection_apply, Module.Basis.extendOfIsLattice_apply, Submodule.mk_eq_top, CStarAlgebra.span_nonneg_inter_ball, groupHomology.isoCycles₁_hom_comp_i, RingTheory.Sequence.isWeaklyRegular_iff, RootPairing.disjoint_rootSpan_ker_rootForm, mem_selfAdjointMatricesSubmodule', groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, Module.End.hasGenEigenvector_iff, Submodule.torsion_isTorsion, Submodule.mapQ_comp, Submodule.Convex.semilinear_range, PeriodPair.analyticOnNhd_weierstrassPExcept, Module.End.invtSubmodule.id, rank_span, Submodule.norm_orthogonalProjection, LinearMap.range_eq_of_proj, LinearEquiv.map_mem_invtSubmodule_iff, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat, Module.Basis.span_eq, Submodule.instHasOrthogonalProjectionTop, AffineSubspace.signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot, Submodule.comap_smul', EuclideanGeometry.orthogonalProjection_mem_orthogonal, Polynomial.degreeLT.basisProd_natAdd, Submodule.torsionBy_isInternal, exteriorPower.presentation_G, Submodule.mem_set_smul, Submodule.goursat_surjective, GradedTensorProduct.tmul_coe_mul_algebraMap_tmul, IsSemisimpleModule.jacobson_eq_bot, groupCohomology.H1π_comp_map, Submodule.lTensorOne_one_tmul, LinearIndependent.sumElim_of_quotient, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, Module.End.mem_genEigenspace_zero, LinearMap.finrank_maxGenEigenspace_eq, LinearMap.IsProj.codRestrict_apply, Submodule.restrictScalarsEmbedding_apply, DirectSum.decomposeLinearEquiv_symm_lof, lipschitzGroup.involute_act_ι_mem_range_ι, AdicCompletion.transitionMap_comp_eval_apply, Representation.coindMap_coe_apply, Polynomial.degreeLE_mono, Submodule.comap_smul'', Submodule.map_coe, Submodule.mem_toSubalgebra, ModuleCat.smulShortComplex_X₃_isModule, LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal, Module.surjective_piEquiv_apply_iff, isIsotypic_iff_isFullyInvariant_imp_bot_or_top, LinearMap.nondegenerate_restrict_of_disjoint_orthogonal, Submodule.le_prod_iff, Submodule.dualAnnihilator_iSup_eq, rank_le_of_isSMulRegular, LinearPMap.coe_vadd, AffineSubspace.mem_direction_iff_eq_vsub_left, Module.Dual.eq_of_preReflection_mapsTo', Submodule.span_range_eq_top_of_injective_of_rank_le, Submodule.finrank_lt, Submodule.dualAnnihilator_eq_bot_iff, TensorProduct.quotTensorEquivQuotSMul_comp_mk, Submodule.rank_sup_add_rank_inf_eq, ZSpan.repr_floor_apply, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, MvPolynomial.homogeneousSubmodule_mul, MeasureTheory.condExpIndSMul_ae_eq_smul, FractionalIdeal.coe_div, rank_top, Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, isNoetherian_range, Submodule.bot_eq_top_of_rank_eq_zero, Submodule.linearProjOfIsCompl_apply_eq_zero_iff, LieAlgebra.IsKilling.span_weight_eq_top, coplanar_iff_finrank_le_two, LieSubalgebra.bot_toSubmodule, Submodule.notMem_span_of_apply_notMem_span_image, LinearMap.tensorKerEquiv_apply, Polynomial.mem_degreeLE, Submodule.span_smul_span, Submodule.map_mem_span_algebraMap_image, IsLocalFrameOn.generating, AdicCompletion.eval_lift_apply, ModuleCat.span_rightExact, Module.Basis.span_neg, Submodule.finite_sup, Submodule.finrank_quotient_le, IsFractionRing.coeSubmodule_injective, LinearMap.range_codRestrict, Submodule.mem_biSup_iff_exists_dfinsupp, Representation.invtSubmodule.coe_bot, TensorProduct.AlgebraTensorModule.range_lTensor_idealMap, exteriorPower.ιMulti_family_linearIndependent_ofBasis, LieSubmodule.toSubmodule_eq_bot, MeasureTheory.lpMeas.ae_fin_strongly_measurable', LinearMap.disjoint_ker', Submodule.span.ringHom_apply, isSMulRegular_iff_ker_lsmul_eq_bot, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, Submodule.map₂_le_map₂_left, groupCohomology.cocyclesMk₀_eq, Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice, Submodule.mem_sup_left, isSemisimpleModule_biSup_of_isSemisimpleModule_submodule, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, Submodule.range_subtype, Submodule.coe_toSubMulAction, range_derivWithin_subset_closure_span_image, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, isArtinian_iSup, vsub_set_subset_vectorSpan, Submodule.one_eq_range, ContinuousLinearMap.finite_dimensional_eigenspace, LinearEquiv.ker, Module.End.genEigenspace_le_genEigenspace_finrank, ClassGroup.equivPic_apply, Submodule.subtype_injective, Submodule.instIsOrderedAddMonoid, NumberField.mixedEmbedding.disjoint_span_commMap_ker, Set.MapsTo.submoduleSpan, LinearPMap.mem_adjoint_domain_of_exists, AdicCompletion.val_zero_apply, Submodule.mem_div_iff_smul_subset, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, Submodule.dualRestrict_apply, LinearMap.BilinForm.finrank_add_finrank_orthogonal, LinearMap.mapsTo_biSup_of_mapsTo, Submodule.smulMemClass, Valuation.leSubmodule_zero, Module.End.mem_genEigenspace, rank_quotient_eq_of_le_torsion, Submodule.comap_op_one, IsSemisimpleModule.exists_linearEquiv_dfinsupp, Submodule.neg_coe, groupHomology.single_mem_cycles₂_iff, Submodule.index_smul_le, HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image, NonUnitalAlgebra.top_toSubmodule, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, Module.Finite.exists_fin_quot_equiv, Submodule.topologicalClosure_iSup_map_single, GradedAlgebra.mem_support_iff, Submodule.finrank_quotient, Submodule.comapSubtypeEquivOfLe_apply_coe, PeriodPair.summable_weierstrassPExceptSummand, RootPairing.RootPositiveForm.algebraMap_posForm, RootPairing.EmbeddedG2.span_eq_top, Subalgebra.pointwise_smul_toSubmodule, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left, Submodule.liftQ_mkQ, Finsupp.ker_lsingle, Submodule.instMulRightMono, AmpleSet.of_one_lt_codim, Submodule.dualAnnihilator_eq_bot_iff', LinearMap.ker_lsmul, groupHomology.boundaries₁_le_cycles₁, ModuleCat.mono_as_hom'_subtype, DirectSum.isInternal_biSup_submodule_of_iSupIndep, QuadraticMap.Nondegenerate.rank_rad_polar_le, HahnEmbedding.Partial.exists_domain_eq_top, Submodule.dfinsuppSumAddHom_mem, Submodule.mem_sup_right, QuotSMulTop.map_id, LinearMap.ker_le_range_iff, PointedCone.ofSubmodule_sup, Submodule.sup_set_smul, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule, Ideal.map_toCotangent_ker, isSMulRegular_on_quot_iff_lsmul_comap_le, Submodule.inf_colon, Submodule.map_op_one, LinearMap.range_le_ker_iff, Submodule.pow_succ', Submodule.Quotient.norm_mk_lt, Module.isPrincipal_def, LinearMap.ofIsCompl_zero, LinearPMap.exists_of_le, Module.Baer.ExtensionOfMaxAdjoin.eqn, Pi.mem_span_range_single_inl_iff, Submodule.span_biInter, Submodule.sup_span, AffineSubspace.equivMapOfInjective_toFun, AffineSubspace.direction_sInf_of_mem_sInf, exteriorPower.ιMulti_family_span, LinearPMap.supSpanSingleton_apply_mk, RootPairing.IsRootSystem.span_coroot_eq_top, ZSpan.fract_eq_fract, Subalgebra.prod_toSubmodule, Submodule.smul_top_le_comap_smul_top, Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero, Submodule.toLocalized'_apply_coe, Submodule.mul_def, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff, EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq, Module.End.invtSubmodule.mk_eq_bot_iff, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Submodule.powSMulQuotInclusion_injective, Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk, LinearMap.BilinForm.finrank_add_finrank_orthogonal', LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, Module.Basis.sumQuot_inl, ZLattice.sum_piFinset_Icc_rpow_le, LinearEquiv.ofInjective_symm_apply, Submodule.ker_liftQ, LieSubalgebra.lie_mem_sup_of_mem_normalizer, Submodule.QuotientTorsion.torsion_eq_bot, Submodule.smul_of_tower_mem, LieAlgebra.Extension.twoCocycleOf_coe_coe, Submodule.mem_map_equiv, Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, ExteriorAlgebra.GradedAlgebra.ι_apply, Submodule.linearProjOfIsCompl_surjective, LinearMap.exists_extend_of_notMem, RootPairing.posRootForm_rootFormIn_posDef, RootPairing.isCompl_corootSpan_ker_corootForm, Module.End.genEigenspace_zero, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, LinearMap.comp_ker_subtype, PointedCone.ofSubmodule_iInf, Submodule.mulMap_range, AddMonoidAlgebra.single_mem_gradeBy, Finsupp.disjoint_supported_supported_iff, weightedVSub_mem_vectorSpan_pair, isFullyInvariant_iff_le_imp_isotypicComponent_le, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, groupHomology.coinvariantsKerOfIsBoundary₀_coe, Affine.Simplex.map_subtype_restrict, Submodule.span_zero, NonUnitalAlgebra.sInf_toSubmodule, exteriorPower.oneEquiv_ιMulti, Module.End.invtSubmodule.comp, LinearMap.ker_eq_bot_range_liftQ_iff, Submodule.map_add_le, Affine.Simplex.restrict_map_subtype, OrthogonalFamily.pairwise, continuous_stereoInvFun, RootPairing.CoPolarizationIn_apply, Submodule.mem_iSup_iff_exists_dfinsupp', LieSubmodule.submodule_span_le_lieSpan, Submodule.LinearDisjoint.linearIndependent_left_of_flat, Submodule.orthogonalProjection_eq_zero_iff, linearDepOn_iff', groupCohomology.cocycles₁_ext_iff, Module.Basis.units_smul_span_eq_top, LinearEquiv.mem_dilatransvections_iff_finrank_quotient, AdicCompletion.eval_surjective, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, ZLattice.covolume.tendsto_card_div_pow'', AdicCompletion.ofPowSMul_val_apply, Polynomial.sylveserMap_comp_adjSylvester, LieAlgebra.IsKilling.ker_killingForm_eq_bot, ClosedSubmodule.toSubmodule_sInf, Submodule.smul_mem_iff'', Module.Basis.mk_eq_spanRank, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', SkewMonoidAlgebra.mem_span_support, Submodule.covBy_span_singleton_sup, groupCohomology.map_H0Iso_hom_f_assoc, Submodule.FG.smul, AffineSubspace.subtypeₐᵢ_toAffineMap, exteriorPower.ιMulti_span, Submodule.map_equivMapOfInjective_symm_apply, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, Polynomial.Chebyshev.U_mem_span_T, Submodule.map_le_localized₀, ClosedSubmodule.coe_sup, Finsupp.supportedEquivFinsupp_symm_apply_coe_apply, Submodule.eq_bot_of_isLocalized₀_span, RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection, LinearMap.ker_single, NonUnitalSubalgebra.coe_toSubmodule, LinearIndependent.isCompl_span_image, Submodule.orthogonalProjection_starProjection_of_le, Submodule.toNonUnitalSubalgebra_mk, LinearMap.finrank_range_add_finrank_ker, Submodule.IsCompl.projection_apply_mem, exteriorPower.toTensorPower_apply_ιMulti, Submodule.coe_orthogonalProjection_apply, ModuleCat.kernelIsoKer_inv_kernel_ι, IsLocalization.coeSubmodule_top, Submodule.toAddSubgroup_le, FractionalIdeal.mem_extended_iff, iSupIndep_range_lsingle, IsIsotypicOfType.isotypicComponent, Submodule.spanRank_eq_of_equiv, Submodule.Quotient.eq', Submodule.coe_matrix, LinearEquiv.mem_stabilizer_submodule_of_le_fixedSubmodule, Module.Finite.exists_fin, Submodule.neg_toAddSubmonoid, Submodule.carrier_eq_coe, LinearMap.le_ker_iff_map, Submodule.torsion'_torsion'_eq_top, groupCohomology.cocycles₁.coe_mk, instModuleFree_of_discrete_submodule, Submodule.wcovBy_span_singleton_sup, PeriodPair.ω₁_mem_lattice, Submodule.starProjection_apply_eq_zero_iff, Submodule.localized'_smul, Module.End.invtSubmodule.bot_mem, Submodule.iInf_comap_proj, UnitAddTorus.span_mFourierLp_closure_eq_top, ContinuousLinearMap.apply_val_ker, ContinuousLinearMap.orthogonal_mem_invtSubmodule, Module.Flat.iff_rTensor_injective', SubmodulesBasis.inter, PeriodPair.analyticOnNhd_weierstrassP, LieSubmodule.iSupIndep_toSubmodule, AddMonoidAlgebra.grade.gradedMonoid, Submodule.Quotient.nontrivial_iff, ModuleCat.imageIsoRange_hom_subtype_apply, skewAdjointPart_comp_subtype_skewAdjoint, RootPairing.eq_top_of_mem_invtSubmodule_of_forall_eq_univ, Module.Basis.mem_span_repr_support, LinearMap.iterateMapComap_le_succ, Submodule.mem_top, Submodule.mem_iSup_of_directed, Submodule.decomposition_erase_inf, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, HasStrictFDerivAt.implicitFunction_apply_image, ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz, LinearMap.ker_eq_bot_of_inverse, Module.End.mem_invtSubmodule_iff_map_le, Submodule.connectedComponentIn_eq_self_of_one_lt_codim, AdicCompletion.transitionMap_map_one, SubmodulesRingBasis.mul, Module.End.invtSubmodule.codisjoint_mk_iff, Module.jacobson_quotient_jacobson, Polynomial.degreeLT.basisProd_castAdd, MvPolynomial.coeffsIn_le, QuotSMulTop.mem_annihilator, ContinuousLinearMap.range_coprod, Submodule.finrank_add_eq_of_isCompl, Submodule.localized'_bot, Finsupp.lmapDomain_disjoint_ker, ModuleCat.epi_iff_range_eq_top, Submodule.FG.generators_mem, Finsupp.supportedEquivFinsupp_apply_apply, Submodule.map_one, Module.Basis.isChain_range_flag, Submodule.toSubMulAction_one, Submodule.height_lt_top, Submodule.FG.rTensor.directLimit_apply', CliffordAlgebra.evenOdd_isCompl, LinearMap.restrict_eq_domRestrict_codRestrict, Submodule.image_smul_top_eq_range_lsum, Submodule.localized₀_inf, MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero, Module.End.genEigenspace_le_smul, Submodule.finiteDimensional_of_le, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure, Submodule.prod_sup_prod, LieModule.Cohomology.d₂₃_comp_d₁₂, isNoetherian_iff, Subspace.quotDualCoannihilatorToDual_bijective, groupHomology.single_mem_cycles₁_iff, LinearMap.ker_tensorProductMk, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, Affine.Simplex.affineSpan_pair_eq_altitude_iff, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, Module.isTorsionBy_iff_torsionBy_eq_top, Representation.invariants_eq_top, Subrepresentation.subrepresentationSubmoduleOrderIso_apply, lTensor_mkQ, AlgHom.equalizer_toSubmodule, Submodule.norm_subtypeL_le, Finsupp.single_mem_supported, Ideal.coe_piOrderIso_apply, Submodule.coe_scott_continuous, IsSemisimpleModule.range, Submodule.pow_toAddSubmonoid, Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson, ContinuousLinearEquiv.fst_equivOfRightInverse, Submodule.comap_top, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, Submodule.coe_eq_univ, Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator, Submodule.instFaithfulVAddSubtypeMem, exteriorPower.zeroEquiv_symm_apply, Affine.Simplex.direction_altitude, Submodule.set_smul_le, Submodule.isAtom_iff_finrank_eq_one, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Submodule.map_injective_of_injective, Module.torsion_by_prime_power_decomposition, Module.AEval.mem_mapSubmodule_apply, Affine.Simplex.restrict_map_inclusion, Ideal.Filtration.iSup_N, Submodule.isOrtho_bot_left, Submodule.basis_of_pid_aux, Submodule.iSup_toAddSubmonoid, Submodule.torsion'_isTorsion', Module.Basis.flag_strictMono, DirectSum.isInternal_submodule_iff_isCompl, Representation.asAlgebraHom_mem_of_forall_mem, Module.le_comap_jacobson, HahnEmbedding.Partial.apply_of_mem_stratum, Subalgebra.pi_toSubmodule, Submodule.exists_norm_eq_iInf_of_complete_subspace, Submodule.restrictScalars_sInf, AdicCompletion.eval_apply, finiteDimensional_direction_affineSpan_singleton, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, Submodule.sndEquiv_apply, Submodule.instSMulCommClassSubtypeMemTorsion', IsSemisimpleModule.quotient, Submodule.localized'_le_localized'_of_smul_le, LinearPMap.adjointAux_inner, Submodule.add_eq_sup, Submodule.sndEquiv_symm_apply_coe, Algebra.idealMap_apply_coe, Submodule.comapSubtypeEquivOfLe_symm_apply, groupCohomology.map_id_comp_H0Iso_hom_assoc, IsLocalization.coeSubmodule_sup, Submodule.le_pow_toAddSubmonoid, Submodule.comap_bot, Module.End.genEigenspace_restrict, Submodule.eq_bot_of_localization₀_maximal, groupCohomology.isoCocycles₂_hom_comp_i_assoc, le_comap_range_rTensor, Matrix.rank_eq_finrank_span_cols, Submodule.Quotient.equiv_trans, EuclideanGeometry.orthogonalProjection_eq_iff_mem, LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup, Submodule.le_traceDual_iff_map_le_one, Subspace.dualAnnihilator_inf_eq, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, Absorbent.subset_range_iff_surjective, Module.Basis.mem_span_iff_repr_mem, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, injective_lTensor_quotient_iff_inf_eq_mul, Submodule.coe_subtypeL, KaehlerDifferential.quotKerTotalEquiv_apply, Submodule.mem_sSup, Representation.mem_invtSubmodule, Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl, AffineMap.linear_eqOn_vectorSpan, KaehlerDifferential.kerTotal_map', Submodule.mulExact_unitsToPic_mapAlgebra, Submodule.bot_colon, Module.Finite.iff_cofg_bot, Submodule.LinearDisjoint.bot_left, ArchimedeanClass.ball_antitone, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, LinearPMap.add_domain, Submodule.annihilator_eq_top_iff, quotient_prod_linearEquiv, LinearMap.domRestrict₁₂_apply, Submodule.sup_toAddSubgroup, RCLike.span_one_I, Submodule.traceDual_top, PeriodPair.ω₂_mem_lattice, Submodule.mem_invtSubmodule_reflection_iff, Submodule.disjoint_torsionBySet_ideal, Ideal.primaryComponent_torsionBySet_of_isCoprime, Ideal.map_includeLeft_eq, LieModule.range_traceForm_le_span_weight, Submodule.mem_graph_toLinearPMap, lieModule_lcs_map_le, AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq, Submodule.restrictScalars_pow, Algebra.Generators.H1Cotangent.equiv_apply, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, LinearMap.IsPerfectCompl.isCompl_left, RingTheory.Sequence.isRegular_cons_iff', groupCohomology.coe_mapCocycles₂, Submodule.mk_eq_zero, Submodule.Quotient.restrictScalarsEquiv_mk, Submodule.orthogonalProjection_norm_le, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, Submodule.sub_mem_iff_right, Submodule.span_le, Submodule.instCovariantClassSetHSMulLe, LinearRecurrence.is_sol_iff_mem_solSpace, LinearMap.BilinForm.le_flip_dualSubmodule, LinearMap.injective_rangeRestrict_iff, Submodule.span_sInf, LinearMap.ker_le_ker_of_range, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_right, LinearMap.quotientInfEquivSupQuotient_surjective, Submodule.mul_mem_mul_rev, Submodule.colon_bot, Module.Basis.is_basis_iff_det, LinearPMap.graph_map_snd_eq_range, ZLattice.comap_span_top, ModuleCat.toKernelSubobject_arrow, LinearPMap.domain_mono, Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator, Submodule.orthogonalProjection_orthogonal, AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty, Submodule.CoFG.sInf_of_finite, LinearMap.finrank_eigenspace_le, Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord, LinearMap.domRestrict_apply, LinearMap.surjective_comp_subtype_of_isComplemented, affineSpan_insert_zero, Submodule.eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator, Polynomial.taylorLinearEquiv_apply_coe, MeasureTheory.norm_condExpL2_le_one, Submodule.mem_mk, LinearMap.mem_span_iff_continuous, Module.finrank_quotient_add_finrank_le, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, Module.Flat.iff_lTensor_injective', groupCohomology.H1π_eq_iff, Submodule.mem_span_insert, DirectSum.decompose_smul, Submodule.map₂_sup_right, SchauderBasis.RankOneDecomposition.e_mem_range, Submodule.toConvexCone_bot, IsFractionRing.ideal_span_singleton_map_subset, Module.Basis.addSubgroupOfClosure_apply, AffineSubspace.vsub_left_mem_direction_iff_mem, Module.End.invtSubmodule.disjoint_iff, Module.End.isSemisimple_iff, MeasureTheory.condExpL2_comp_continuousLinearMap, Subspace.isCompl_dualAnnihilator, Submodule.mapsTo_span, Polynomial.mem_degreeLT, ZSpan.setFinite_inter, LinearEquiv.ofTop_apply, Submodule.bot_toAddSubgroup, PeriodPair.derivWeierstrassPExcept_def, groupCohomology.isoCocycles₁_hom_comp_i_assoc, Submodule.mulMap_comp_rTensor, Submodule.coe_set_neg, Algebra.Extension.Cotangent.ker_mk, Submodule.torsionBySet_isTorsionBySet, Submodule.IsPrimary.mem_or_mem, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero, Submodule.isOrtho_sup_left, AdicCompletion.val_sum_apply, ClosedSubmodule.coe_toSubmodule, Submodule.span_neg_eq_neg, Polynomial.degreeLT.basis_repr, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection, ZLattice.coe_comap, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, Submodule.isPrimary_finsetInf, Submodule.map_div, Module.Basis.eval_ker, LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate, LinearIsometry.submoduleMap_apply_coe, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left, CStarAlgebra.span_unitary, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top, ContinuousLinearMap.mem_invtSubmodule_adjoint_iff, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, AddMonoidAlgebra.mem_gradeBy_iff, Ideal.primaryComponent_torsionBySet_eq_inf, LinearEquiv.reduce_mkQ, Submodule.orthogonalProjection_eq_linearProjOfIsCompl, LinearPMap.adjoint_apply_of_dense, groupHomology.mapCycles₁_quotientGroupMk'_epi, Submodule.Quotient.mk_eq_zero, RootPairing.range_polarizationIn_le_span_coroot, lipschitzGroup.conjAct_smul_range_ι, groupHomology.mapCycles₁_comp_i_assoc, Submodule.exists_smith_normal_form_of_le, linearDepOn_iff'ₛ, Submodule.map_inf_le, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum, MeasureTheory.condExpL2_const_inner, LinearPMap.toFun_eq_coe, exteriorPower.ιMulti_family_apply_coe, IsAdicComplete.StrictMono.mkQ_comp_lift, Submodule.instNonemptySubtypeSetEqSpan, Module.erange_coe, Submodule.map_subtype_le, IsCoercive.isClosed_range, LinearMap.quotKerEquivOfSurjective_apply_mk, Submodule.mem_traceDual_iff_isIntegral, Submodule.Quotient.nontrivial_of_lt_top, ZSpan.ceil_eq_self_of_mem, AffineEquiv.ofEq_rfl, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, IsLocalization.mem_span_iff, LinearMap.finiteDimensional_range, Submodule.le_dualCoannihilator_dualAnnihilator, MvPolynomial.range_evalᵢ, Submodule.coe_prodEquivOfClosedCompl, Module.Basis.restrictScalars_toMatrix, Submodule.sub_mem, TensorProduct.exists_of_fg, Submodule.torsionBy.mk_smul, AddMonoidAlgebra.mem_span_support, Subalgebra.rank_toSubmodule, Submodule.comap_liftQ, groupHomology.π_comp_H2Iso_inv_apply, Submodule.mem_torsion'_iff, LinearMap.BilinForm.restrict_apply, groupCohomology.coboundariesOfIsCoboundary₂_coe, Submodule.topologicalClosure.completeSpace, Submodule.toSubMulAction_injective, IsLocalization.coeSubmodule_injective, DirectSum.range_coeLinearMap, Submodule.submoduleOf_self, LinearPMap.mem_range_iff, Submodule.lt_top_of_finrank_lt_finrank, Subalgebra.fg_bot_toSubmodule, EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq, MonoidAlgebra.mem_supported', HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source, HasStrictFDerivAt.eq_implicitFunction, IsLocalRing.spanFinrank_eq_finrank_quotient, Finsupp.range_restrictDom, Submodule.starProjection_eq_self_iff, LinearEquiv.fixedReduce_mkQ, QuadraticMap.mem_radical_iff', Projectivization.Subspace.mem_submodule_iff, LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal, linearIndepOn_iff_linearCombinationOnₛ, Submodule.finiteDimensional_inf_left, Submodule.Quotient.mk_zero, Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, EuclideanGeometry.Sphere.finrank_orthRadius, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, LinearMap.rank_range_add_rank_ker, finrank_vectorSpan_insert_le_set, Submodule.smul_mem, Submodule.coe_equivMapOfInjective_apply, Submodule.mem_neg, Submodule.mem_iSup, AdicCompletion.of_apply, Submodule.starProjection_tendsto_closure_iSup, Submodule.ker_unitsMap_spanSingleton, LinearMap.exists_map_addHaar_eq_smul_addHaar', InnerProductSpace.gramSchmidt_mem_span, HomogeneousSubmodule.toSubmodule_injective, MvPolynomial.mem_restrictTotalDegree, iSupIndep_iff_forall_dfinsupp, groupCohomology.coboundaries₁.coe_mk, LieModule.coe_lowerCentralSeries_ideal_le, IsLinearTopology.hasBasis_right_ideal, Submodule.comap_sup_of_injective, Submodule.comap_unop_mul, Submodule.disjoint_iff_comap_eq_bot, groupHomology.mem_cycles₁_iff, LinearMap.range_add_le, MvPolynomial.restrictTotalDegree_le_restrictDegree, instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace, LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, Subspace.finrank_add_finrank_dualAnnihilator_eq, TensorProduct.toLinearMap_mapInclIsometry, Submodule.span_eq_iSup_of_singleton_spans, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, Submodule.small_sup, FiniteArchimedeanClass.mem_closedBall_iff, Submodule.existsUnique_add_of_isCompl_prod, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, lsum_comp_mapRange_toSpanSingleton, IsAdicComplete.StrictMono.mk_lift, MvPolynomial.coe_coeffsIn, RootPairing.algebraMap_root'In_apply, groupCohomology.mapCocycles₁_comp_i, Module.isTorsionBy_quotient_element_smul, groupHomology.boundariesToCycles₁_apply, orthonormal_span, groupHomology.single_mem_cycles₂_iff_inv, Submodule.pow_one, OrthogonalFamily.projection_directSum_coeAddHom, LinearEquiv.range, TensorProduct.range_mapIncl_mono, surjective_stereographic, Module.Finite.of_isComplemented_codomain, MatrixModCat.fromMatrixLinear_apply_coe, Submodule.mem_closure_iff, TensorProduct.spanRank_top_le, Submodule.coe_ofLinearComb, Submodule.coe_toAddSubgroup, PeriodPair.finrank_lattice, PeriodPair.derivWeierstrassP_add_coe, linearIndepOn_iff_linearCombinationOn, Module.IsTorsionBy.quotient, Submodule.piQuotientLift_mk, Module.Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra, ArchimedeanClass.closedBall_top, LinearMap.toKerIsLocalized_apply_coe, Submodule.coe_sInf, LinearMap.submoduleMap_surjective, hasFDerivAt_stereoInvFunAux_comp_coe, Submodule.isGLB_sInf, Submodule.range_fst, LinearMap.finrank_le_of_isSMulRegular, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, LinearIsometryEquiv.ofEq_symm, AffineSubspace.isClosed_direction_iff, finiteDimensional_vectorSpan_insert, LinearPMap.inverse_domain, Submodule.neg_le_neg, exteriorPower.basis_repr_self, LieSubmodule.inf_toSubmodule, MeasureTheory.condExpL2_indicator_nonneg, NonUnitalAlgebra.iInf_toSubmodule, Ideal.exists_pow_inf_eq_pow_smul, Submodule.flip_quotDualCoannihilatorToDual_injective, Submodule.coe_prodEquivOfClosedCompl_symm, Submodule.isClosed_or_dense_of_isCoatom, groupCohomology.cocycles₁.d₁₂_apply, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule, Submodule.mulRightMap_apply_single, MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid, Subspace.dualPairing_eq, Submodule.span_iUnion₂, groupHomology.isoCycles₂_hom_comp_i_assoc, Submodule.toSubMulAction_mono, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, LinearMap.prod_eq_sup_map, subalgebra_top_rank_eq_submodule_top_rank, Submodule.mapQ_id, Int.submodule_toAddSubgroup_index_ne_zero_iff, Submodule.fstEquiv_apply, Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply, groupCohomology.π_comp_H2Iso_hom, Submodule.restrictScalars_inf, AdicCompletion.eval_comp_of, FiniteDimensional.span_singleton, Ideal.to_quotient_square_comp_toCotangent, Submodule.factor_comp_mk, DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def, groupHomology.H2π_eq_zero_iff, finrank_vectorSpan_range_le, Submodule.fg_unit, GeneralSchauderBasis.finrank_range_proj, Submodule.restrictScalars_localized'_smul, FractionalIdeal.inv_of_ne_zero, Module.Basis.sumQuot_repr_inr, ContinuousLinearEquiv.ofSubmodules_apply, AdicCompletion.val_smul_apply, AffineSubspace.coe_direction_eq_vsub_set_right, Submodule.colon_inf_eq_left_of_subset, Submodule.add_mem, Submodule.smul_mono_left, BoxIntegral.unitPartition.tag_mem_smul_span, LinearMap.ofIsCompl_eq_add, Module.Dual.range_eq_top_of_ne_zero, PointedCone.mem_lineal, LinearPMap.IsClosable.existsUnique, FractionalIdeal.coe_zero, Submodule.span_range_inclusionSpan, PeriodPair.weierstrassPExcept_add, LinearMap.surjective_domRestrict_iff, Submodule.coe_iSup_of_chain, Submodule.span_coe_eq_restrictScalars, Module.mapEvalEquiv_symm_apply, iSupIndep.subtype_ne_bot_le_finrank_aux, Submodule.surjOn_iff_le_map, ZLattice.exists_finsetSum_norm_rpow_le_tsum, Submodule.map₂_le_map₂_right, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, Submodule.unitsQuotEquivRelPic_apply_coe, Subspace.dualEquivDual_apply, Submodule.isHilbertSumOrthogonal, Submodule.instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀, Affine.Simplex.restrict_points_coe, Submodule.pointwiseCentralScalar, Submodule.map_le_smul_top, Submodule.smul_coe, Polynomial.Chebyshev.T_derivative_mem_span_T, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, ZLattice.abs_repr_le, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, LinearMap.singularValues_eq_zero_iff_le_finrank_range, DirectSum.IsInternal.collectedBasis_repr_of_mem, Affine.Simplex.excenterExists_restrict, MvPolynomial.decomposition.decompose'_eq, Submodule.restrictScalarsEquiv_apply, ZLattice.covolume_eq_det, Finsupp.iSup_lsingle_range, RingFilterBasis.SubmodulesBasis.smul, Representation.invtSubmodule.bot_mem, Submodule.mul_bot, Submodule.instIsScalarTower, Finsupp.mem_supported', rank_range_of_surjective, Submodule.card_eq_card_quotient_mul_card, Module.finrank_le_one_iff_top_isPrincipal, groupHomology.δ₁_apply, Submodule.LinearDisjoint.linearIndependent_mul_of_flat, Submodule.quotientQuotientEquivQuotientAux_mk_mk, LinearIndepOn.quotient_iff_union, LinearMap.ker_le_comap, LinearMap.restrict_apply, AddMonoidAlgebra.mem_supported, Submodule.factor_surjective, LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self, Submodule.mem_toNonUnitalSubalgebra, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, Submodule.Quotient.equiv_apply, Submodule.natAbs_det_basis_change, Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup, Submodule.orthogonalProjectionFn_mem, groupHomology.H1π_eq_iff, Submodule.one_eq_span, Submodule.nonempty_basis_of_pid, Module.End.injOn_iInf_maxGenEigenspace, LinearMap.range_lt_top_of_det_eq_zero, LinearMap.comap_le_comap_iff, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker, LinearIsometryEquiv.submoduleMap_apply_coe, LinearMap.isProj_iff_isIdempotentElem, Submodule.cardQuot_apply, LinearPMap.image_iff, LinearMap.BilinForm.isCompl_span_singleton_orthogonal, Submodule.spanFinrank_eq_iInf, AdicCompletion.eval_lift, Submodule.comap_subtype_le_iff, Submodule.finiteDimensional_iSup, ZModModule.exists_submodule_subset_card_le, MeasureTheory.lpMeas.aestronglyMeasurable, Submodule.disjoint_span_singleton'', Submodule.eq_top_of_finrank_eq, Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq, Submodule.mem_iff_norm_starProjection, Submodule.range_liftQ, isSemisimpleModule_iff_exists_linearEquiv_dfinsupp, groupHomology.cyclesMap_comp_isoCycles₁_hom, vectorSpan_of_subsingleton, PeriodPair.differentiableOn_derivWeierstrassPExcept, LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top, IsDedekindDomain.flat_iff_torsion_eq_bot, Submodule.le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot, ContinuousLinearEquiv.ofSubmodules_symm_apply, Submodule.le_comap_pow_of_le_comap, LinearMap.card_support_singularValues, Submodule.neg_le, HilbertBasis.finite_spans_dense, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective, Submodule.comap_map_eq, exists_linearIndepOn_id_extension, KaehlerDifferential.kerTotal_mkQ_single_algebraMap, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun, HahnEmbedding.Partial.toOrderAddMonoidHom_injective

---

← Back to Index