Defs

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

Statistics

Metric	Count
Definitions generator, gi, span, unexpander, «term_∙_»	5
Theorems of_span, of_span₀, isPrincipal_iff, of_surjective, isPrincipal_def, isPrincipal_submodule_iff, principal, span_singleton_generator, closure_induction, closure_le_toAddSubmonoid_span, closure_subset_span, codisjoint_iff_exists_add_eq, coe_iSup_of_chain, coe_iSup_of_directed, coe_span_eq_self, coe_sup, eq_span_singleton_of_surjective, exists_mem_sup, forall_mem_sup, iSup_eq_span, iSup_eq_span', iSup_span, instIsPrincipalSpanSingletonSet, isPrincipal_iff, le_span_singleton_iff, lt_sup_iff_notMem, mem_iSup, mem_iSup_of_chain, mem_iSup_of_directed, mem_sSup, mem_sSup_of_directed, mem_span, mem_span_finite_of_mem_span, mem_span_insert, mem_span_insert', mem_span_of_mem, mem_span_pair, mem_span_singleton, mem_span_singleton_self, mem_span_singleton_trans, mem_span_triple, mem_sup, mem_sup', nontrivial_span_singleton, span_attach_biUnion, span_biInter, span_biUnion, span_closure, span_empty, span_eq, span_eq_bot, span_eq_closure, span_eq_iSup_of_singleton_spans, span_eq_of_le, span_eq_span, span_iUnion, span_iUnion₂, span_induction, span_induction₂, span_insert, span_insert_eq_span, span_insert_zero, span_int_eq, span_int_eq_addSubgroupClosure, span_int_eq_addSubgroup_closure, span_inter, span_le, span_mono, span_monotone, span_nat_eq, span_nat_eq_addSubmonoidClosure, span_nat_eq_addSubmonoid_closure, span_range_eq_iSup, span_range_update_add_smul, span_range_update_sub_smul, span_sInf, span_sInf_le, span_sSup, span_sSup', span_sdiff_singleton_zero, span_setOf_mem_eq_top, span_singleton_eq_bot, span_singleton_eq_range, span_singleton_eq_top_iff, span_singleton_group_smul_eq, span_singleton_le_iff_mem, span_singleton_smul_eq, span_singleton_smul_le, span_smul_le, span_span, span_span_coe_preimage, span_sup, span_union, span_univ, span_zero, span_zero_singleton, submodule_eq_sSup_le_nonzero_spans, subset_span, subset_span_finite_of_subset_span, subset_span_trans, sup_eq_top_iff, sup_span, sup_toAddSubgroup, sup_toAddSubmonoid	104
Total	109

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_span 📖	mathematical	Disjoint Submodule Submodule.instPartialOrder Submodule.instOrderBot Submodule.span	Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.disjoint_iff_forall_ne Submodule.disjoint_def Submodule.subset_span
of_span₀ 📖	mathematical	Disjoint Submodule Submodule.instPartialOrder Submodule.instOrderBot Submodule.span Set Set.instMembership AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Set.diff_singleton_eq_self of_span

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipal_iff 📖	mathematical	—	Module.IsPrincipal	—	RingHomInvPair.ids Module.IsPrincipal.of_surjective surjective

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipal_def 📖	mathematical	—	IsPrincipal Submodule.IsPrincipal Top.top Submodule Submodule.instTop	—	—
isPrincipal_submodule_iff 📖	mathematical	—	IsPrincipal Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.IsPrincipal	—	le_antisymm Submodule.mem_span_singleton Submodule.span_singleton_le_iff_mem Submodule.mem_span_singleton_self top_unique Eq.le

Module.IsPrincipal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_surjective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Module.IsPrincipal	—	Submodule.IsPrincipal.principal top_unique Submodule.mem_span_singleton Eq.le map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Submodule.smul_mem Submodule.mem_span_singleton_self

Submodule

Definitions

Name	Category	Theorems
gi 📖	CompOp	—
span 📖	CompOp	713 math math: LinearMap.eqOn_span', mem_colon_span_singleton, disjoint_span_singleton', continuousOn_stereoToFun, span_nat_eq_addSubmonoid_closure, RootPairing.posRootForm_posForm_apply_apply, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, integralClosure_le_span_dualBasis, finrank_span_finset_eq_card, 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, span_sInf_le, RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', span_span_of_tower, RootPairing.Base.span_coroot_support, rank_le_card_isVisible, AddMonoidAlgebra.of'_mem_span, set_smul_span, RootPairing.EmbeddedG2.mem_span_of_mem_allRoots, 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, InnerProductSpace.span_gramSchmidtNormed_range, ExteriorAlgebra.ιMulti_span_fixedDegree, Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span, mem_orthogonal_singleton_iff_inner_right, BoxIntegral.unitPartition.mem_smul_span_iff, injective_inclusionSpan, LinearIndepOn.span_image_extend_eq_span_image, Span.repr_def, starProjection_singleton, Fintype.mem_span_image_iff_exists_fun, 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, 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', reflection_singleton_apply, rank_span_set, RootPairing.RootPositiveForm.zero_lt_posForm_iff, mem_ideal_smul_span_iff_exists_sum', linearIndepOn_id_union_iff, coeff_minpolyDiv_sub_pow_mem_span, InnerProductSpace.gramSchmidt_def, coe_dualCoannihilator_span, FiniteDimensional.span_of_finite, closure_le_toAddSubmonoid_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, FiniteDimensional.mem_span_of_iInf_ker_le_ker, BoxIntegral.unitPartition.integralSum_eq_tsum_div, 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, ZSpan.quotientEquiv_apply_mk, 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, 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.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, linearIndependent_fin_cons, SymmetricPower.span_tprod_eq_top, LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis, 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, 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, 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, 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, LinearMap.range_toSpanSingleton, 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', 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, 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, 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, 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, span_int_eq_addSubgroup_closure, ZSpan.isAddFundamentalDomain', linearIndependent_fin_succ', LinearIndepOn.notMem_span_of_insert, span_eq, span_set_smul, rank_span_finset_le, 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, instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, KaehlerDifferential.kerTotal_map, spanSingleton_apply, span_eq_closure, Module.Basis.mem_span_image, annihilator_span_singleton, closure_subset_span, span_selfAdjoint, ZSpan.span_top, IsLattice.span_eq_top, 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, vectorSpan_segment, ZSpan.map, 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, 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, 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', 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, 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, map₂_span_singleton_eq_map, disjoint_span_singleton_of_notMem, isQuotientEquivQuotientPrime_iff, LinearEquiv.coord_self, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, fg_iff_exists_fin_generating_family, annihilator_span, Algebra.adjoin_eq_span, span_union, 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_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, starProjection_orthogonalComplement_singleton_eq_zero, span_lt_of_subset_of_card_lt_finrank, mem_span_of_mem, iSup_eq_span', mem_span, 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, 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, Module.Basis.localizationLocalization_span, LinearMap.span_singleton_inf_orthogonal_eq_bot, exists_maximal_linearIndepOn, span_singleton_eq_one_iff, NonUnitalStarAlgebra.span_eq_toSubmodule, isNoetherian_span_of_finite, IsPrincipal.span_singleton_generator, 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, 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, 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, smul_span, 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, 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, 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, TensorProduct.map_range_eq_span_tmul, 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, span_range_eq_top_of_injective_of_rank_le, ZSpan.repr_floor_apply, LieAlgebra.IsKilling.span_weight_eq_top, span_smul_span, IsLocalFrameOn.generating, 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, span_zero, RootPairing.Base.span_int_coroot_support, continuous_stereoInvFun, LieSubmodule.submodule_span_le_lieSpan, SkewMonoidAlgebra.mem_span_support, covBy_span_singleton_sup, exteriorPower.ιMulti_span, PeriodPair.lattice_eq_span_range_basis, 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, 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', RCLike.span_one_I, LieModule.range_traceForm_le_span_weight, span_le, span_sInf, Module.Basis.is_basis_iff_det, affineSpan_insert_zero, Finsupp.lcomapDomain_eq_linearProjOfIsCompl, LinearMap.mem_span_iff_continuous, mem_span_insert, 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, 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, span_generators, 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
«term_∙_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_induction 📖	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid zero_mem span AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup add_mem SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smul_mem subset_span Submodule SetLike.instMembership setLike	—	—	zero_mem add_mem smul_mem subset_span AddSubmonoid.closure_induction AddSubmonoid.subset_closure AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubmonoid.instAddSubmonoidClass
closure_le_toAddSubmonoid_span 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder AddSubmonoid.instPartialOrder AddSubmonoid.closure toAddSubmonoid span	—	closure_subset_span
closure_subset_span 📖	mathematical	—	Set Set.instHasSubset SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure Submodule setLike span	—	AddSubmonoid.closure_le subset_span
codisjoint_iff_exists_add_eq 📖	mathematical	—	Codisjoint Submodule instPartialOrder instOrderTop SetLike.instMembership setLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	codisjoint_iff eq_top_iff' mem_sup
coe_iSup_of_chain 📖	mathematical	—	SetLike.coe Submodule setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder instPartialOrder OrderHom.instFunLike Set.iUnion	—	coe_iSup_of_directed Monotone.directed_le SemilatticeSup.instIsDirectedOrder OrderHom.monotone
coe_iSup_of_directed 📖	mathematical	Directed Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.coe setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set.iUnion	—	AddSubmonoid.coe_iSup_of_directed Set.mem_iUnion smul_mem' le_antisymm iSup_le le_iSup Set.iUnion_subset
coe_span_eq_self 📖	mathematical	—	SetLike.coe Submodule setLike span	—	le_antisymm AddMemClass.add_mem AddSubmonoidClass.toAddMemClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SMulMemClass.smul_mem span_le le_rfl subset_span
coe_sup 📖	mathematical	—	SetLike.coe Submodule setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.ext SetLike.mem_coe mem_sup Set.mem_add
eq_span_singleton_of_surjective 📖	mathematical	Submodule SetLike.instMembership setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Semiring.toModule module LinearMap.instFunLike	span Set Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_antisymm mem_span_singleton IsScalarTower.left coe_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_eq_mul mul_one span_le
exists_mem_sup 📖	mathematical	—	Submodule SetLike.instMembership setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
forall_mem_sup 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
iSup_eq_span 📖	mathematical	—	iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice span Set.iUnion SetLike.coe setLike	—	span_eq
iSup_eq_span' 📖	mathematical	—	iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice span Set.iUnion SetLike.coe setLike	—	iSup_congr_Prop span_eq
iSup_span 📖	mathematical	—	iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice span Set.iUnion	—	le_antisymm iSup_le span_mono Set.subset_iUnion span_le Set.iUnion_subset mem_iSup_of_mem subset_span
instIsPrincipalSpanSingletonSet 📖	mathematical	—	IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule span Set Set.instSingletonSet	—	—
isPrincipal_iff 📖	mathematical	—	IsPrincipal span Set Set.instSingletonSet	—	—
le_span_singleton_iff 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span Set Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	instIsConcreteLE
lt_sup_iff_notMem 📖	mathematical	—	Submodule Preorder.toLT PartialOrder.toPreorder instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice span Set Set.instSingletonSet SetLike.instMembership setLike	—	—
mem_iSup 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	span_singleton_le_iff_mem le_iSup_iff
mem_iSup_of_chain 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice DFunLike.coe OrderHom Nat.instPreorder PartialOrder.toPreorder instPartialOrder OrderHom.instFunLike	—	mem_iSup_of_directed Monotone.directed_le SemilatticeSup.instIsDirectedOrder OrderHom.monotone
mem_iSup_of_directed 📖	mathematical	Directed Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	SetLike.mem_coe coe_iSup_of_directed Set.mem_iUnion
mem_sSup 📖	mathematical	—	Submodule SetLike.instMembership setLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	sSup_eq_iSup
mem_sSup_of_directed 📖	mathematical	Set.Nonempty Submodule DirectedOn Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership setLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set Set.instMembership	—	Set.Nonempty.to_subtype sSup_eq_iSup' mem_iSup_of_directed DirectedOn.directed_val
mem_span 📖	mathematical	—	Submodule SetLike.instMembership setLike span	—	Set.mem_iInter₂
mem_span_finite_of_mem_span 📖	mathematical	Submodule SetLike.instMembership setLike span	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	—	span_induction Finset.coe_singleton Set.singleton_subset_iff mem_span_singleton_self Finset.coe_empty span_empty AddSubmonoidClass.toZeroMemClass addSubmonoidClass Finset.coe_union Set.union_subset span_union mem_sup smul_mem
mem_span_insert 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instInsert AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	span_insert
mem_span_insert' 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike span Set Set.instInsert AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mem_span_insert neg_smul add_assoc add_neg_cancel_comm_assoc add_comm add_neg_cancel_right
mem_span_of_mem 📖	mathematical	Set Set.instMembership	Submodule SetLike.instMembership setLike span	—	subset_span
mem_span_pair 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instInsert Set.instSingletonSet AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
mem_span_singleton 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	span_induction one_smul zero_smul add_smul smul_smul smul_mem subset_span
mem_span_singleton_self 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instSingletonSet	—	subset_span
mem_span_singleton_trans 📖	—	Submodule SetLike.instMembership setLike span Set Set.instSingletonSet	—	—	SetLike.mem_coe Set.singleton_subset_iff subset_span_trans
mem_span_triple 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instInsert Set.instSingletonSet AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mem_span_insert add_assoc
mem_sup 📖	mathematical	—	Submodule SetLike.instMembership setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	span_induction AddSubmonoidClass.toZeroMemClass addSubmonoidClass add_zero zero_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass add_assoc add_comm smul_mem smul_add span_union span_eq le_sup_left le_sup_right
mem_sup' 📖	mathematical	—	Submodule SetLike.instMembership setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	mem_sup
nontrivial_span_singleton 📖	mathematical	—	Nontrivial Submodule SetLike.instMembership setLike span Set Set.instSingletonSet	—	mem_span_singleton_self mk_eq_zero
span_attach_biUnion 📖	mathematical	—	span SetLike.coe Finset Finset.instSetLike Finset.biUnion Finset.instMembership Finset.attach iSup Submodule SetLike.instMembership ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	Finset.coe_biUnion Set.iUnion_congr_Prop Finset.coe_attach Set.iUnion_true span_iUnion
span_biInter 📖	mathematical	—	span Set.iInter Submodule Set Set.instMembership SetLike.coe setLike InfSet.sInf instInfSet	—	coe_sInf span_eq
span_biUnion 📖	mathematical	—	span Set.iUnion Submodule Set Set.instMembership SetLike.coe setLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	Set.sUnion_image GaloisInsertion.l_sSup_u_image
span_closure 📖	mathematical	—	span SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	le_antisymm span_le closure_subset_span span_mono AddSubmonoid.subset_closure
span_empty 📖	mathematical	—	span Set Set.instEmptyCollection Bot.bot Submodule instBot	—	GaloisConnection.l_bot GaloisInsertion.gc
span_eq 📖	mathematical	—	span SetLike.coe Submodule setLike	—	span_eq_of_le Set.Subset.refl subset_span
span_eq_bot 📖	mathematical	—	span Bot.bot Submodule instBot AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	eq_bot_iff mem_bot subset_span span_le
span_eq_closure 📖	mathematical	—	toAddSubmonoid span AddSubmonoid.closure AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.univ	—	le_antisymm span_induction AddSubmonoid.subset_closure one_smul ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubmonoid.instAddSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubmonoid.closure_induction SemigroupAction.mul_smul smul_zero smul_add AddSubmonoid.closure_le smul_mem subset_span
span_eq_iSup_of_singleton_spans 📖	mathematical	—	span iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set Set.instMembership Set.instSingletonSet	—	Set.biUnion_of_singleton
span_eq_of_le 📖	—	Set Set.instHasSubset SetLike.coe Submodule setLike Preorder.toLE PartialOrder.toPreorder instPartialOrder span	—	—	le_antisymm span_le
span_eq_span 📖	—	Set Set.instHasSubset SetLike.coe Submodule setLike span	—	—	le_antisymm span_le
span_iUnion 📖	mathematical	—	span Set.iUnion iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
span_iUnion₂ 📖	mathematical	—	span Set.iUnion iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	GaloisConnection.l_iSup₂ GaloisInsertion.gc
span_induction 📖	—	subset_span AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid zero_mem span AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup add_mem SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smul_mem Submodule SetLike.instMembership setLike	—	—	subset_span zero_mem add_mem smul_mem span_le
span_induction₂ 📖	—	subset_span AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ZeroMemClass.zero_mem Submodule setLike AddSubmonoidClass.toZeroMemClass addSubmonoidClass span AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smul_mem SetLike.instMembership	—	—	subset_span ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass addSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass smul_mem span_induction
span_insert 📖	mathematical	—	span Set Set.instInsert Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Set.instSingletonSet	—	Set.insert_eq span_union
span_insert_eq_span 📖	mathematical	Submodule SetLike.instMembership setLike span	Set Set.instInsert	—	span_eq_of_le Set.insert_subset_iff subset_span span_mono Set.subset_insert
span_insert_zero 📖	mathematical	—	span Set Set.instInsert AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	le_antisymm span_le Set.insert_subset_iff subset_span span_mono Set.subset_insert
span_int_eq 📖	mathematical	—	toAddSubgroup Int.instRing AddCommGroup.toIntModule span Int.instSemiring AddCommGroup.toAddCommMonoid SetLike.coe AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike	—	span_int_eq_addSubgroupClosure AddSubgroup.closure_eq
span_int_eq_addSubgroupClosure 📖	mathematical	—	toAddSubgroup Int.instRing AddCommGroup.toIntModule span Int.instSemiring AddCommGroup.toAddCommMonoid AddSubgroup.closure AddCommGroup.toAddGroup	—	AddSubgroup.closure_eq_of_le subset_span span_induction AddSubgroup.subset_closure AddSubgroup.zero_mem AddSubgroup.add_mem AddSubgroup.zsmul_mem
span_int_eq_addSubgroup_closure 📖	mathematical	—	toAddSubgroup Int.instRing AddCommGroup.toIntModule span Int.instSemiring AddCommGroup.toAddCommMonoid AddSubgroup.closure AddCommGroup.toAddGroup	—	span_int_eq_addSubgroupClosure
span_inter 📖	mathematical	—	span Set Set.instInter SetLike.coe Submodule setLike instMin	—	GaloisInsertion.l_inf_u
span_le 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span Set Set.instHasSubset SetLike.coe setLike	—	Set.Subset.trans subset_span mem_span
span_mono 📖	mathematical	Set Set.instHasSubset	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span	—	span_le Set.Subset.trans subset_span
span_monotone 📖	mathematical	—	Monotone Set Submodule PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder span	—	span_mono
span_nat_eq 📖	mathematical	—	toAddSubmonoid Nat.instSemiring AddCommMonoid.toNatModule span SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike	—	span_nat_eq_addSubmonoidClosure AddSubmonoid.closure_eq
span_nat_eq_addSubmonoidClosure 📖	mathematical	—	toAddSubmonoid Nat.instSemiring AddCommMonoid.toNatModule span AddSubmonoid.closure AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	AddSubmonoid.closure_eq_of_le subset_span GaloisConnection.l_le OrderIso.to_galoisConnection span_le AddSubmonoid.subset_closure
span_nat_eq_addSubmonoid_closure 📖	mathematical	—	toAddSubmonoid Nat.instSemiring AddCommMonoid.toNatModule span AddSubmonoid.closure AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	span_nat_eq_addSubmonoidClosure
span_range_eq_iSup 📖	mathematical	—	span Set.range iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set Set.instSingletonSet	—	span_eq_iSup_of_singleton_spans iSup_range
span_range_update_add_smul 📖	mathematical	—	span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.range Function.update AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	le_antisymm eq_or_ne Function.update_self AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass subset_span smul_mem Function.update_of_ne add_sub_cancel_right sub_mem addSubgroupClass
span_range_update_sub_smul 📖	mathematical	—	span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.range Function.update SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	sub_eq_add_neg neg_smul span_range_update_add_smul
span_sInf 📖	mathematical	—	span SetLike.coe Submodule setLike InfSet.sInf instInfSet	—	span_eq
span_sInf_le 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span Set.sInter InfSet.sInf instInfSet Set.image Set	—	le_sInf span_mono Set.sInter_subset_of_mem
span_sSup 📖	mathematical	—	span Set.sUnion SupSet.sSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set.image Set	—	le_antisymm span_le le_sSup Set.mem_image_of_mem subset_span sSup_le span_mono Set.subset_sUnion_of_mem
span_sSup' 📖	mathematical	—	span SetLike.coe Submodule setLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	span_eq
span_sdiff_singleton_zero 📖	mathematical	—	span Set Set.instSDiff Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	span_insert_zero Set.insert_diff_self_of_mem Set.diff_singleton_eq_self
span_setOf_mem_eq_top 📖	mathematical	—	span Submodule SetLike.instMembership setLike addCommMonoid module setOf Set Set.instMembership Top.top instTop	—	span_span_coe_preimage
span_singleton_eq_bot 📖	mathematical	—	span Set Set.instSingletonSet Bot.bot Submodule instBot AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
span_singleton_eq_range 📖	mathematical	—	SetLike.coe Submodule setLike span Set Set.instSingletonSet Set.range SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.ext mem_span_singleton
span_singleton_eq_top_iff 📖	mathematical	—	span Set Set.instSingletonSet Top.top Submodule instTop SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	eq_top_iff le_span_singleton_iff
span_singleton_group_smul_eq 📖	mathematical	—	span Set Set.instSingletonSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	le_antisymm span_singleton_smul_le inv_smul_smul
span_singleton_le_iff_mem 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span Set Set.instSingletonSet SetLike.instMembership setLike	—	span_le Set.singleton_subset_iff SetLike.mem_coe
span_singleton_smul_eq 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	span Set Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction	—	CanLift.prf instCanLiftUnitsValIsUnit Units.smul_def span_singleton_group_smul_eq Units.instIsScalarTower IsScalarTower.left
span_singleton_smul_le 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span Set Set.instSingletonSet	—	span_le Set.singleton_subset_iff SetLike.mem_coe smul_of_tower_mem mem_span_singleton_self
span_smul_le 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder span Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	span_le smul_mem subset_span
span_span 📖	mathematical	—	span SetLike.coe Submodule setLike	—	span_eq
span_span_coe_preimage 📖	mathematical	—	span Submodule SetLike.instMembership setLike addCommMonoid module Set.preimage Top.top instTop	—	eq_top_iff span_induction subset_span ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass addSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass smul_mem
span_sup 📖	mathematical	—	Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice span Set Set.instUnion SetLike.coe setLike	—	span_union span_eq
span_union 📖	mathematical	—	span Set Set.instUnion Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	GaloisConnection.l_sup GaloisInsertion.gc
span_univ 📖	mathematical	—	span Set.univ Top.top Submodule instTop	—	eq_top_iff SetLike.le_def instIsConcreteLE subset_span
span_zero 📖	mathematical	—	span Set Set.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Bot.bot Submodule instBot	—	Set.singleton_zero span_singleton_eq_bot
span_zero_singleton 📖	mathematical	—	span Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Bot.bot Submodule instBot	—	ext smul_zero Zero.instNonempty
submodule_eq_sSup_le_nonzero_spans 📖	mathematical	—	SupSet.sSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice setOf SetLike.instMembership setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid span Set Set.instSingletonSet	—	le_antisymm AddSubmonoidClass.toZeroMemClass addSubmonoidClass le_sSup mem_span_singleton_self sSup_le_iff span_singleton_le_iff_mem
subset_span 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Submodule setLike span	—	mem_span
subset_span_finite_of_subset_span 📖	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Submodule setLike span	—	—	Finset.induction_on Finset.coe_empty span_empty instIsEmptyFalse Finset.coe_insert mem_span_finite_of_mem_span Finset.mem_insert_self Finset.coe_union span_union mem_sup_right HasSubset.Subset.trans Set.instIsTransSubset le_sup_left
subset_span_trans 📖	—	Set Set.instHasSubset SetLike.coe Submodule setLike span	—	—	GaloisConnection.le_u_l_trans GaloisInsertion.gc
sup_eq_top_iff 📖	mathematical	—	Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Top.top instTop SetLike.instMembership setLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	eq_top_iff' mem_sup
sup_span 📖	mathematical	—	Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice span Set Set.instUnion SetLike.coe setLike	—	span_union span_eq
sup_toAddSubgroup 📖	mathematical	—	toAddSubgroup Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instCompleteLattice	—	AddSubgroup.ext mem_toAddSubgroup mem_sup AddSubgroup.mem_sup
sup_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instCompleteLattice	—	AddSubmonoid.ext mem_toAddSubmonoid mem_sup AddSubmonoid.mem_sup

Submodule.IsPrincipal

Definitions

Name	Category	Theorems
generator 📖	CompOp	21 math math: Submodule.isInternal_prime_power_torsion_of_pid, contentIdeal_generator_dvd_coeff, Ideal.span_singleton_generator, mem_iff_eq_smul_generator, generator_submoduleImage_dvd_of_mem, FractionalIdeal.mul_generator_self_inv, dvd_generator_iff, generator_map_dvd_of_mem, Ideal.associatesEquivIsPrincipal_symm_apply, FractionalIdeal.eq_spanSingleton_of_principal, dvd_generator_span_iff, generator_mem, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, eq_bot_iff_generator_eq_zero, prime_generator_of_isPrime, span_singleton_generator, associated_generator_span_self, contentIdeal_generator_dvd, mem_iff_generator_dvd, Ideal.prime_generator_of_prime, Ideal.isoBaseOfIsPrincipal_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
principal 📖	mathematical	—	Submodule.span Set Set.instSingletonSet	—	—
span_singleton_generator 📖	mathematical	—	Submodule.span Set Set.instSingletonSet generator	—	principal

Submodule.span

Definitions

Name	Category	Theorems
unexpander 📖	CompOp	—

---

← Back to Index