span π | CompOp | 791 mathmath: LinearMap.eqOn_span', mem_colon_span_singleton, disjoint_span_singleton', continuousOn_stereoToFun, RootPairing.posRootForm_posForm_apply_apply, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, integralClosure_le_span_dualBasis, finrank_span_finset_eq_card, Polynomial.Sequence.span_degreeLE, finrank_span_set_eq_card, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, smul_def, vectorSpan_range_eq_span_range_vsub_left_ne, InnerProductSpace.span_gramSchmidtNormed, linearIndependent_option, span_subset_span, tendsto_tsum_div_pow_atTop_integral, affineSpan_le_toAffineSubspace_span, NumberField.canonicalEmbedding.mem_span_latticeBasis, linearIndepOn_iff_notMem_span, mem_ideal_smul_span_iff_exists_sum, Module.Basis.coe_span_apply, span_sInf_le, RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', span_span_of_tower, RootPairing.Base.span_coroot_support, rank_le_card_isVisible, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, AddMonoidAlgebra.of'_mem_span, set_smul_span, RootPairing.EmbeddedG2.mem_span_of_mem_allRoots, IsLocalization.smul_mem_finsetIntegerMultiple_span, ZSpan.floor_eq_self_of_mem, tensorEquivSpan_apply_tmul, IsLocalization.coeSubmodule_span, Module.Basis.mem_span, Module.Relations.Solution.surjective_Ο_iff_span_eq_top, span_fourier_closure_eq_top, Polynomial.Sequence.span, RootPairing.restrictScalars_coe_coroot, LinearPMap.domain_supSpanSingleton, LinearIndepOn.notMem_span, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, span_setOf_mem_eq_top, spanFinrank_span_le_ncard_of_finite, Profinite.NobelingProof.Products.span_nil_eq_top, TensorProduct.span_tmul_eq_top, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, Finsupp.instCountableSubtypeMemSubmoduleSpanRange, LinearIndependent.linearCombination_repr, NonUnitalAlgebra.span_eq_toSubmodule, RootPairing.Base.root_mem_span_int, smul_mem_span_smul, MonoidAlgebra.supported_eq_span_single, Module.Basis.mk_repr, Finsupp.span_single_eq_top, InnerProductSpace.span_gramSchmidtNormed_range, ExteriorAlgebra.ΞΉMulti_span_fixedDegree, Module.Basis.groupSMul_span_eq_top, Module.Relations.Solution.injective_fromQuotient_iff_ker_Ο_eq_span, codisjoint_span_image_of_codisjoint, mem_orthogonal_singleton_iff_inner_right, BoxIntegral.unitPartition.mem_smul_span_iff, injective_inclusionSpan, LinearIndepOn.span_image_extend_eq_span_image, span_insert_eq_span, Span.repr_def, starProjection_singleton, Fintype.mem_span_image_iff_exists_fun, RootPairing.invtRootSubmodule.eq_span_root, Projectivization.submodule_eq, RootPairing.span_orbit_eq_top, mem_smul_span_singleton, UnitAddTorus.mFourierSubalgebra_coe, vectorSpan_eq_span_vsub_set_right_ne, LieSubalgebra.submodule_span_le_lieSpan, mem_span_image_iff_exists_fun, ZSpan.smul, exteriorPower.ΞΉMulti_family_span_fixedDegree_of_span, Ideal.submodule_span_eq, span_pow, LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton, FractionalIdeal.coe_extendedHomβ_eq_span, map_span_le, closure_subset_topologicalClosure_span, Module.exists_smul_eq_zero_and_mk_eq, span_smul_eq_of_isUnit, CStarAlgebra.span_nonneg_inter_unitBall, Finsupp.mem_span_iff_linearCombination, spanRank_toENat_eq_iInf_encard, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, range_vecMulLinear, RootPairing.span_coroot'_eq_top, LieSubmodule.lieIdeal_oper_eq_linear_span', mem_span_singleton_trans, reflection_singleton_apply, rank_span_set, RootPairing.RootPositiveForm.zero_lt_posForm_iff, SchauderBasis.range_proj_eq_span, mem_ideal_smul_span_iff_exists_sum', Submonoid.adjoin_eq_span_of_eq_span, linearIndepOn_id_union_iff, coeff_minpolyDiv_sub_pow_mem_span, InnerProductSpace.gramSchmidt_def, coe_dualCoannihilator_span, FiniteDimensional.span_of_finite, closure_le_toAddSubmonoid_span, exteriorPower.ΞΉMulti_span_of_span, MonoidAlgebra.of_mem_span_of_iff, Module.equiv_directSum_of_isTorsion, RootPairing.injOn_dualMap_subtype_span_root_coroot, RootPairing.restrictScalars_pairing, Algebra.adjoin_span, LinearMap.span_singleton_sup_orthogonal_eq_top, span_range_inclusion_restrictScalars_eq_top, FractionalIdeal.isFractional_span_iff, span_eq_of_le, FiniteDimensional.mem_span_of_iInf_ker_le_ker, BoxIntegral.unitPartition.integralSum_eq_tsum_div, span_eq_top_localization_localization, ExteriorAlgebra.ΞΉMulti_span, Algebra.span_le_adjoin, LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot, span_singleton_eq_top_iff, tendsto_card_div_pow_atTop_volume, apply_mem_span_image_iff_mem_span, span_smul_le, Finsupp.span_le_supported_biUnion_support, Finsupp.span_image_eq_map_linearCombination, RootPairing.RootPositiveForm.posForm_apply_root_root_le_zero_iff, ZSpan.quotientEquiv_apply_mk, LinearIndependent.repr_eq_single, Finsupp.supported_eq_span_single, vectorSpan_range_eq_span_range_vsub_right, rank_submodule_le_one_iff, AffineSubspace.direction_affineSpan_insert, mem_span_finset, LinearMap.range_smulRight_apply_of_surjective, KaehlerDifferential.span_range_map_derivation_of_isLocalization, LinearEquiv.toSpanNonzeroSingleton_homothety, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, Profinite.NobelingProof.GoodProducts.spanFin, Ideal.isIdempotentElem_iff_of_fg, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LinearIndependent.disjoint_span_image, RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule, submodule_eq_sSup_le_nonzero_spans, span_nat_eq, RootPairing.Base.coroot_mem_span_int, LinearMap.span_preimage_le, stereographic_apply_neg, finite_span_isCompactElement, LinearIndependent.span_eq_top_of_card_eq_finrank', spanRank_span_of_linearIndepOn, LinearMap.span_inl_union_inr, spanRank_span_le_card, AddSubmonoid.toNatSubmodule_closure, LinearMap.BilinForm.dualSubmodule_span_of_basis, CStarAlgebra.span_nonneg, NumberField.Units.span_basisOfIsMaxRank, range_stereographic_symm, isOpenEmbedding_stereographic_symm, Set.Finite.submoduleSpan, span_le_restrictScalars, smul_mem_span_smul_of_mem, linearIndependent_sum, basisOfLinearIndependentOfCardEqFinrank_repr_apply, span_attach_biUnion, Ideal.Quotient.span_singleton_one, span_eq_bot, Module.Relations.range_map, Matrix.cRank_toNat_eq_finrank, span_mul_span, RootPairing.corootSpan_map_flip_toPerfPair, span_int_eq, FiniteDimensional.span_finset, reflection_orthogonalComplement_singleton_eq_neg, LinearIsometryEquiv.reflections_generate_dim_aux, LinearIndependent.iSupIndep_span_singleton, isArtinian_span_of_finite, LieAlgebra.Basis.coe_cartan_eq_span, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', UniqueDiffWithinAt.dense_tangentConeAt, fg_def, ZSpan.repr_ceil_apply, surjective_tensorToSpan, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, Convex.span_tangentConeAt, finrank_span_le_card, span_coeff_minpolyDiv, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, Module.Basis.span_repr_eq_single, linearIndependent_fin_cons, SymmetricPower.span_tprod_eq_top, LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis, span_range_inclusion_eq_top, contDiffOn_stereoToFun, image_span_subset_span, MonoidAlgebra.mem_span_support, stereoInvFun_apply, disjoint_span_singleton, iSup_span, exists_span_set_card_eq_spanRank, fg_iff_exists_finite_generating_family, ContinuousLinearMap.eqOn_closure_span, span_singleton_algebraMap_of_isUnit, KaehlerDifferential.span_range_derivation, mem_span_singleton, vectorSpan_image_eq_span_vsub_set_left_ne, Ideal.Quotient.smul_top, localized'_span, Module.isTorsionBySet_span_singleton_iff, CStarAlgebra.span_nonneg_inter_unitClosedBall, LinearIsometryEquiv.reflections_generate, NumberField.mixedEmbedding.span_idealLatticeBasis, LinearMap.submoduleOf_span_singleton_of_mem, Field.span_map_pow_expChar_pow_eq_top_of_isSeparable, mem_span_iff_exists_finset_subset, mem_span_mul_finite_of_mem_mul, singleton_span_isCompactElement, span_prod_le, span_range_eq_iSup, LinearIndepOn.subset_span_extend, TopologicalSpace.IsSeparable.span, span_algebraMap_image, LinearIndependent.linearCombinationEquiv_apply_coe, RootPairing.rootSpan_map_toPerfPair, subset_span_trans, Module.Relations.Solution.range_Ο, Affine.Simplex.mongePlane_def, iSupIndep_iff_linearIndependent_of_ne_zero, Module.Basis.span_apply, vectorSpan_eq_span_vsub_finset_right_ne, exteriorPower.ΞΉMulti_span_fixedDegree_of_span_eq_top, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, Module.range_piEquiv, LinearIndependent.linearCombination_comp_repr, RootPairing.corootSpan_dualAnnihilator_map_eq, Algebra.adjoin_nonUnitalSubalgebra_eq_span, atom_iff_nonzero_span, exists_linearIndepOn_extension, LinearMap.range_dualMap_dual_eq_span_singleton, span_val_image_eq_iff, LinearMap.range_toSpanSingleton, RKHS.kerFun_dense, Matrix.eRank_toNat_eq_finrank, Module.Basis.ofZLatticeBasis_span, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Projectivization.submodule_mk, stereoToFun_apply, uniqueDiffWithinAt_iff, NumberField.mixedEmbedding.mem_span_latticeBasis, fg_span_iff_fg_span_finset_subset, coe_tensorSpanEquivSpan_apply_tmul, LieSubmodule.mem_baseChange_iff, PowerBasis.mem_span_pow', span_eq_top_of_span_eq_top, NonUnitalStarAlgebra.adjoin_eq_span, vectorSpan_pair_rev, rank_submodule_le_one_iff', finrank_orthogonal_span_singleton, inclusionSpan_apply_coe, small_span_singleton, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, LinearMap.span_singleton_sup_ker_eq_top, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, RootPairing.GeckConstruction.span_range_h'_eq_top, span_singleton_toAddSubgroup_eq_zmultiples, RootPairing.posRootForm_posForm_pos_of_ne_zero, span_singleton_eq_bot, span_univ, nonzero_span_atom, ModuleCat.span_exact, spanFinrank_span_le_encard, span_image_linearEquiv, traceDual_le_span_map_traceDual, linearIndependent_span, span_range_eq_top_iff_surjective_fintypeLinearCombination, mem_span_set, prod_span, Subalgebra.adjoin_eq_span_basis, vectorSpan_eq_span_vsub_set_left_ne, LinearMap.mem_span_iff_continuous_of_finite, minpoly.ker_aeval_eq_span_minpoly, HilbertBasis.dense_span, Matrix.rank_eq_finrank_span_row, Module.mem_support_iff_exists_annihilator, smul_starProjection_singleton, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, mem_mul_span_singleton, mem_span_finset', mem_span_singleton_self, mapβ_eq_span_image2, Module.Basis.restrictScalars_repr_apply, ConvexCone.IsGenerating.top_le_span, prod_span_singleton, NumberField.Units.regOfFamily_of_isMaxRank, Finsupp.span_eq_range_linearCombination, Finsupp.isCompl_range_lmapDomain_span, affineSpan_subset_span, span_preimage_eq, ContinuousMap.adjoin_id_eq_span_one_union, exists_linearIndependent, RootPairing.IsG2.span_eq_rootSpan_int, Ideal.Quotient.torsionBy_eq_span_singleton, Finsupp.linearCombinationOn_range, colon_span, HomogeneousLocalization.Away.span_mk_prod_pow_eq_top, ZSpan.coe_floor_self, sup_span_singleton_eq_top_iff, AffineSubspace.direction_sup, Matrix.range_mulVecLin, baseChange_eq_span, LinearEquiv.toSpanNonzeroSingleton_apply, instIsZLatticeRealSpan, mem_span_insert', span_algebraMap_image_of_tower, LinearIndependent.notMem_span, vectorSpan_pair, Matrix.range_toLin', LinearIsometryEquiv.toSpanUnitSingleton_apply, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, LinearIndependent.span_repr_eq, norm_inner_eq_norm_tfae, mapβ_span_singleton_eq_map_flip, injective_tensorToSpan, Module.Basis.restrictScalars_apply, LinearPMap.domain_mkSpanSingleton, Module.Basis.flag_succ, Profinite.NobelingProof.GoodProducts.span, ContinuousLinearMap.range_smulRight_apply, map_subtype_span_singleton, ZSpan.isAddFundamentalDomain', linearIndependent_fin_succ', LinearIndepOn.notMem_span_of_insert, span_eq, span_set_smul, rank_span_finset_le, mem_span_insert_exchange, Affine.Simplex.direction_mongePlane, Ideal.Filtration.submodule_span_single, finrank_span_eq_card, starProjection_unit_singleton, LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis, RootPairing.IsRootSystem.span_root_eq_top, RootPairing.zero_le_posForm, PowerBasis.mem_span_pow, ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply, reflection_sub, exists_fun_fin_finrank_span_eq, EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq, instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, KaehlerDifferential.kerTotal_map, spanSingleton_apply, span_eq_closure, Module.Basis.mem_span_image, annihilator_span_singleton, mem_span_mul_finite_of_mem_span_mul, closure_subset_span, span_selfAdjoint, ZSpan.span_top, IsLattice.span_eq_top, Algebra.adjoin_eq_span_of_subset, RootPairing.Base.span_int_root_support, RootPairing.iInf_ker_root'_eq, vectorSpan_eq_span_vsub_set_left, LinearMap.eqOn_span_iff, NumberField.mixedEmbedding.span_latticeBasis, linearIndependent_fin_snoc, LinearIndepOn.mem_span_iff_id, stereographic_neg_apply, InnerProductSpace.gramSchmidt_def', localized'_eq_span, Fintype.range_linearCombination, isPrincipal_iff, mem_span_finite_of_mem_span, vectorSpan_segment, ZSpan.map, AddMonoidAlgebra.supported_eq_span_single, isOrtho_span, ZSpan.exist_unique_vadd_mem_fundamentalDomain, Module.Finite.span_singleton, span_eq_iUnion_nat, instIsPrincipalSpanSingletonSet, le_span_singleton_iff, span_le_span_iff, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, Span.finsupp_linearCombination_repr, mem_span_iff_of_fintype, span_sSup, InnerProductGeometry.angle_eq_angle_add_angle_iff, toENat_rank_span_set, iSup_eq_span, span_int_eq_addSubgroupClosure, RootPairing.iInf_ker_coroot'_eq, LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero, mem_span_singleton_mul, multiple_mem_span_of_mem_localization_span, span_lt_top_of_card_lt_finrank, span_iUnion, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, exists_linearIndependent', span_range_natDegree_eq_adjoin, LinearIndependent.linearCombinationEquiv_symm_apply, ZSpan.isAddFundamentalDomain, abs_signedDist_eq_dist_iff_vsub_mem_span, Module.Relations.Solution.isPresentation_iff, mapβ_span_span, InnerProductSpace.span_gramSchmidt_Iic, DividedPowerAlgebra.submodule_span_prod_dp_eq_top, rank_span_le, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, rank_submodule_eq_one_iff, cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt, linearIndependent_fin_succ, one_eq_span_one_set, Polynomial.span_of_finite_le_degreeLT, IsIntegralClosure.range_le_span_dualBasis, bot_colon', exteriorPower.ΞΉMulti_family_span_of_span, LinearIndependent.span_eq_top_of_card_eq_finrank, maximal_orthonormal_iff_orthogonalComplement_eq_bot, top_le_span_range_iff_forall_exists_fun, Module.injOn_dualMap_subtype_span_range_range, fourierSubalgebra_coe, nontrivial_span_singleton, spanRank_toENat_eq_iInf_finset_card, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, subset_span_finite_of_subset_span, span_range_update_sub_smul, LinearMap.map_span, coord_norm', RootPairing.algebraMap_posRootForm_posForm, KaehlerDifferential.submodule_span_range_eq_ideal, Profinite.NobelingProof.spanFinBasis.span, RootPairing.span_root'_eq_top, Finsupp.linearCombination_restrict, linearIndepOn_union_iff, FractionalIdeal.mem_span_mul_finite_of_mem_mul, LinearIndependent.repr_range, range_deriv_subset_closure_span_image, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, spanFinrank_singleton, LinearPMap.supSpanSingleton_apply_smul_self, RootPairing.restrictScalars_coe_root, mem_span_range_iff_exists_fun, stereographic_target, Finsupp.range_linearCombination, LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, Module.Relations.ker_toQuotient, vectorSpan_range_eq_span_range_vsub_right_ne, Polynomial.Chebyshev.T_iterate_derivative_mem_span_T, mapβ_span_singleton_eq_map, disjoint_span_singleton_of_notMem, isQuotientEquivQuotientPrime_iff, span_eq_top_of_isLocalizedModule, LinearEquiv.coord_self, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, fg_iff_exists_fin_generating_family, annihilator_span, Algebra.adjoin_eq_span, span_union, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, span_fourierLp_closure_eq_top, PrincipalIdealRing.isMaximal_of_irreducible, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, span_range_update_add_smul, LinearIndepOn.mem_span_iff, RootPairing.RootPositiveForm.isSymm_posForm, TensorProduct.range_map_eq_span_tmul, Module.equiv_free_prod_directSum, torsionBySet_span_singleton_eq, smul_one_eq_span, span_singleton_smul_eq, mem_span_image_finset_iff_exists_fun, exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot, mem_annihilator_span, InnerProductSpace.mem_span_gramSchmidt, span_smul, FractionalIdeal.isFractional_span_singleton, CStarAlgebra.span_nonneg_inter_closedBall, range_mfderiv_coe_sphere, image_span_subset, LinearIndepOn.notMem_span_iff_id, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, stereographic_source, IsIntegral.mem_span_pow, span_nat_eq_addSubmonoidClosure, mem_span_pair, mem_span_of_iInf_ker_le_ker, LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul, IsZLattice.span_top, LinearIndepOn.span_extend_eq_span, Module.Basis.self_mem_span_image, vectorSpan_def, traceDual_eq_span_map_traceDual_of_linearDisjoint, spanRank_span_range_of_linearIndependent, Module.End.span_orbit_mem_invtSubmodule, LinearMap.range_liftBaseChange, coe_span_eq_span_of_surjective, Module.FinitePresentation.out, exists_finset_span_eq_linearIndepOn, finrank_span_eq_finrank_span, mem_smul_span, span_zero_singleton, FractionalIdeal.spanFinset_coe, ZSpan.quotientEquiv.symm_apply, coe_dualAnnihilator_span, NumberField.mem_span_integralBasis, IsLocalRing.span_eq_top_of_tmul_eq_basis, apply_mem_span_image_of_mem_span, starProjection_orthogonalComplement_singleton_eq_zero, span_lt_of_subset_of_card_lt_finrank, mem_span_of_mem, iSup_eq_span', LinearIndependent.repr_eq, mem_span, Ideal.FinrankQuotientMap.span_eq_top, pow_eq_span_pow_set, NumberField.mem_span_basisOfFractionalIdeal, LinearIndepOn.image_subset_span_image_extend, eq_span_singleton_of_surjective, liftQSpanSingleton_apply, Finsupp.mem_span_range_iff_exists_finsupp, rank_span_of_finset, span_mono, MvPolynomial.coeffsIn_eq_span_monomial, InnerProductSpace.span_gramSchmidt, ModuleCat.disjoint_span_sum, ConvexCone.IsGenerating.span_eq_top, Finsupp.single_mem_span_single, EuclideanGeometry.hasFDerivAt_inversion, LinearIndependent.repr_ker, top_le_span_of_exact_of_retraction, ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, OrthonormalBasis.span_apply, span_sSup', mem_span_triple, IsSimpleModule.span_singleton_eq_top, ContinuousMap.adjoin_id_eq_span_one_add, Ideal.range_finsuppTotal, lt_sup_iff_notMem, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, vectorSpan_image_eq_span_vsub_set_right_ne, span_sdiff_singleton_zero, finrank_span_eq_finrank, RootPairing.posRootForm_posForm_nondegenerate, mem_span_image_finset_iff_exists_fun', Module.Basis.localizationLocalization_span, LinearMap.span_singleton_inf_orthogonal_eq_bot, exists_maximal_linearIndepOn, span_singleton_eq_one_iff, Subalgebra.adjoin_eq_span_of_eq_span, NonUnitalStarAlgebra.span_eq_toSubmodule, isNoetherian_span_of_finite, IsPrincipal.span_singleton_generator, EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq, span_span, Profinite.NobelingProof.GoodProducts.span_iff_products, tensorToSpan_apply_tmul, InnerProductSpace.span_gramSchmidt_Iio, linearIndependent_iff_notMem_span, mem_orthogonal_singleton_iff_inner_left, span_flip_eq_top_iff_linearIndependent, Polynomial.degreeLT_eq_span_X_pow, span_biUnion, span_singleton_eq_range, LinearEquiv.toSpanNonzeroSingleton_one, LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis, LinearIsometryEquiv.reflections_generate_dim, fg_span_singleton, span_inter, small_span, coe_span_eq_self, span_span_coe_preimage, LieSubmodule.lieIdeal_oper_eq_linear_span, MvPolynomial.homogeneousSubmodule_one_eq_span_X, span_range_eq_top_iff_surjective_finsuppLinearCombination, LinearMap.map_span_le, finrank_span_singleton, LieAlgebra.mem_corootSpace', span_sup, span_singleton_mul, stereographic_apply, RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff, IsLocalRing.CotangentSpace.span_image_eq_top_iff, LinearEquiv.coord_apply_smul, RootPairing.restrictScalars_toLinearMap_apply_apply, mem_span_set', linearIndepOn_union_iff_quotient, FractionalIdeal.coe_spanSingleton, TensorProduct.AlgebraTensorModule.ker_mapOfCompatibleSMul, span_closure, LinearIndepOn.notMem_span_iff, Module.Relations.Solution.span_relation_le_ker_Ο, UnitAddTorus.span_mFourier_closure_eq_top, FG.span, LinearIndependent.notMem_span_image, smul_mem_span_smul', StarAlgebra.adjoin_eq_span, Polynomial.span_le_degreeLE_of_finite, span_eq_top_of_ne_zero, ZSpan.discreteTopology_pi_basisFun, mul_eq_span_mul_set, span_empty, RootPairing.Base.span_root_support, GeneralSchauderBasis.range_proj_eq_span, smul_span, RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff, signedDist_eq_dist_iff_vsub_mem_span, AffineSubspace.direction_perpBisector, RootPairing.posRootForm_posForm_anisotropic, AddMonoidAlgebra.mem_span_support', setSemiring_smul_def, linearIndepOn_insert, Module.Finite.span_finset, subset_span, cyclotomic_comp_X_add_one_isEisensteinAt, span_singleton_le_iff_mem, ContinuousLinearEquiv.coord_norm', LinearMap.mem_span_iff_bound, traceDual_span_of_basis, tendsto_card_div_pow_atTop_volume', IsLocalization.span_invSubmonoid, LinearMap.isCompl_span_singleton_orthogonal, FractionalIdeal.spanSingleton_def, Module.Finite.span_of_finite, Finsupp.span_single_image, vectorSpan_eq_span_vsub_set_right, map_span, coe_torsion_eq_annihilator_ne_bot, RootPairing.span_root_image_eq_top_of_forall_orthogonal, PiTensorProduct.span_tprod_eq_top, finrank_eq_one_iff_of_nonzero, span_preimage_le, Module.Basis.ofIsLocalizedModule_span, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, linearIndependent_option', linearIndepOn_id_insert, range_ker_disjoint, Finsupp.range_lmapDomain, RootPairing.rootSpan_dualAnnihilator_map_eq, span_singleton_smul_le, span_insert, span_range_subtype_eq_top_iff, isCompl_span_singleton_of_isCoatom_of_notMem, IsLocalizedModule.smul_mem_finsetIntegerMultiple_span, Finsupp.mem_span_image_iff_linearCombination, ZSpan.vadd_mem_fundamentalDomain, span_monotone, finset_span_isCompactElement, ZSpan.fract_apply, LieAlgebra.mem_corootSpace, span_image, NonUnitalAlgebra.adjoin_toSubmodule, mem_annihilator_span_singleton, ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe, mem_span_set_iff_exists_finsupp_le_finrank, ContinuousLinearEquiv.coord_self, LinearMap.range_smulRight_apply, ContinuousLinearEquiv.coord_norm, AddSubgroup.toIntSubmodule_closure, CStarAlgebra.span_nonneg_inter_ball, EuclideanGeometry.Sphere.direction_orthRadius, rank_span, Module.Basis.span_eq, baseChange_span, FG.exists_span_set_encard_eq_spanFinrank, Module.surjective_piEquiv_apply_iff, Module.Dual.eq_of_preReflection_mapsTo', span_range_eq_top_of_injective_of_rank_le, ZSpan.repr_floor_apply, LieAlgebra.IsKilling.span_weight_eq_top, notMem_span_of_apply_notMem_span_image, span_smul_span, map_mem_span_algebraMap_image, IsLocalFrameOn.generating, ModuleCat.span_rightExact, Module.Basis.span_neg, MvPolynomial.restrictSupport_eq_span, span.ringHom_apply, range_derivWithin_subset_closure_span_image, NumberField.mixedEmbedding.disjoint_span_commMap_ker, Set.MapsTo.submoduleSpan, RootPairing.RootPositiveForm.algebraMap_posForm, RootPairing.EmbeddedG2.span_eq_top, LinearMap.span_singleton_eq_range, Polynomial.degreeLE_eq_span_X_pow, Module.Basis.constr_range, Pi.mem_span_range_single_inl_iff, span_biInter, sup_span, exteriorPower.ΞΉMulti_family_span, LinearPMap.supSpanSingleton_apply_mk, RootPairing.IsRootSystem.span_coroot_eq_top, ZSpan.fract_eq_fract, mul_def, exteriorPower.ΞΉMulti_span_fixedDegree, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, LieSubalgebra.lie_mem_sup_of_mem_normalizer, span_zero, RootPairing.Base.span_int_coroot_support, continuous_stereoInvFun, LieSubmodule.submodule_span_le_lieSpan, Module.Basis.units_smul_span_eq_top, SkewMonoidAlgebra.mem_span_support, covBy_span_singleton_sup, exteriorPower.ΞΉMulti_span, Polynomial.Chebyshev.U_mem_span_T, PeriodPair.lattice_eq_span_range_basis, LinearIndependent.isCompl_span_image, FractionalIdeal.mem_extended_iff, fg_span, Module.Finite.exists_fin, vectorSpan_range_eq_span_range_vsub_left, wcovBy_span_singleton_sup, UnitAddTorus.span_mFourierLp_closure_eq_top, span_eq_span, Module.mem_support_iff_of_span_eq_top, Module.Basis.mem_span_repr_support, LinearMap.orthogonal_span_singleton_eq_to_lin_ker, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Module.torsion_by_prime_power_decomposition, span_singleton_eq_span_singleton, FG.spanRank_le_iff_exists_span_set_card_le, Matrix.rank_eq_finrank_span_cols, Module.Basis.mem_span_iff_repr_mem, Module.Relations.Solution.IsPresentation.ker_Ο, KaehlerDifferential.kerTotal_map', Polynomial.Sequence.span_degreeLT, RCLike.span_one_I, LieModule.range_traceForm_le_span_weight, span_le, span_sInf, lift_spanRank_le_iff_exists_span_set_card_le, Module.Basis.is_basis_iff_det, ZLattice.comap_span_top, affineSpan_insert_zero, Finsupp.lcomapDomain_eq_linearProjOfIsCompl, LinearMap.mem_span_iff_continuous, mem_span_insert, IsFractionRing.ideal_span_singleton_map_subset, mapsTo_span, ZSpan.setFinite_inter, IsPrincipal.principal, orthogonalProjection_orthogonalComplement_singleton_eq_zero, span_neg_eq_neg, CStarAlgebra.span_unitary, PiTensorProduct.map_range_eq_span_tprod, instNonemptySubtypeSetEqSpan, ZSpan.ceil_eq_self_of_mem, IsLocalization.mem_span_iff, Module.Basis.restrictScalars_toMatrix, torsionBy.mk_smul, AddMonoidAlgebra.mem_span_support, span_neg, linearIndepOn_iff_linearCombinationOnβ, InnerProductSpace.gramSchmidt_mem_span, span_eq_iSup_of_singleton_spans, orthonormal_span, span_singleton_group_smul_eq, surjective_stereographic, linearIndepOn_iff_linearCombinationOn, hasFDerivAt_stereoInvFunAux_comp_coe, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, span_iUnionβ, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, FiniteDimensional.span_singleton, span_insert_zero, BoxIntegral.unitPartition.tag_mem_smul_span, span_range_inclusionSpan, span_coe_eq_restrictScalars, Polynomial.Chebyshev.T_derivative_mem_span_T, span_generators, span_smul_of_span_eq_top, NonUnitalAlgebra.adjoin_eq_span, LinearIndepOn.quotient_iff_union, FractionalIdeal.coe_extended_eq_span, Module.Relations.Solution.ofQuotient_Ο, one_eq_span, restrictScalars_span, LinearMap.BilinForm.isCompl_span_singleton_orthogonal, spanFinrank_eq_iInf, disjoint_span_singleton'', LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top, IsLocalization.coeSubmodule_span_singleton, HilbertBasis.finite_spans_dense, exists_linearIndepOn_id_extension
|