LinearIndependent

📁 Source: Mathlib/RingTheory/Algebraic/LinearIndependent.lean

Statistics

Metric	Count
Definitions LinearIndependent	1
Theorems linearIndependent_sub_inv	1
Total	2

Transcendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIndependent_sub_inv 📖	mathematical	Transcendental Field.toCommRing DivisionRing.toRing Field.toDivisionRing	LinearIndependent InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule	—	linearIndependent_iff' Polynomial.X_sub_C_ne_zero IsSimpleRing.instNontrivial DivisionRing.isSimpleRing transcendental_iff Polynomial.aeval_sub Polynomial.aeval_X Polynomial.aeval_C Finset.prod_erase_mul mul_inv_cancel_right₀ Finset.sum_congr mul_smul_comm Algebra.to_smulCommClass Finset.mul_sum MulZeroClass.mul_zero map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Finset.prod_congr map_sub Algebra.smul_def Finset.mem_erase_of_ne_of_mem Finset.ne_of_mem_erase sub_self eq_zero_of_ne_zero_of_mul_right_eq_zero IsDomain.to_noZeroDivisors Field.isDomain Finset.prod_ne_zero_iff sub_ne_zero zero_add Finset.sum_eq_zero Finset.sum_erase_add map_zero MonoidWithZeroHomClass.toZeroHomClass

(root)

Definitions

Name	Category	Theorems
LinearIndependent 📖	MathDef	279 math math: linearIndependent_set_coe_iff, Orthonormal.linearIndependent, LinearIndependent.sum_type, Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent, linearIndependent_of_top_le_span_of_card_le_finrank, Module.Basis.ofVectorSpaceIndex.linearIndependent, DFinsupp.linearIndependent_single_iff, natCast_le_rank_iff_finset, exists_linearIndependent_snoc_of_lt_finrank, LinearIndependent.pair_iff, Fintype.linearIndependent_iffₒₛ, IntermediateField.LinearDisjoint.linearIndependent_right', linearIndependent_option, linearIndependent_iff_card_le_finrank_span, LinearIndependent.pair_add_smul_right_iff, exists_linearIndependent_of_le_finrank, LinearIndependent.pair_add_smul_left_iff, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_left, Ideal.iSupIndep.linearIndependent', exteriorPower.ιMulti_family_linearIndependent_field, RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero, RootPairing.linearIndependent_of_sub_mem_range_root', Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, ModuleCat.linearIndependent_shortExact, LinearIndependent.of_isLocalizedModule_of_isRegular, Pi.linearIndependent_single, Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left, linearIndependent_iff_injective_finsuppLinearCombination, LinearIndependent.of_subsingleton', sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent, LinearMap.linearIndependent_of_isOrthoᵢ, linearIndependent_neg_iff, Fintype.linearIndependent_iff', LinearIndepOn.linearIndependent_restrict, RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent, InnerProductSpace.gramSchmidtNormed_linearIndependent, linearIndependent_of_top_le_span_of_card_eq_finrank, exists_linearIndependent_of_le_rank, linearIndepOn_univ_iff, LinearIndependent.map_of_surjective_injectiveₛ, linearIndependent_unique, RootPairing.Base.linearIndependent_pair_of_ne, affineIndependent_set_iff_linearIndependent_vsub, linearIndepOn_univ, Matrix.linearIndependent_rows_of_invertible, linearIndependent_iff_ker, exists_linearIndependent_cons_of_lt_finrank, Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval, linearIndependent_iUnion_finite, LinearIndependent.group_smul_iff, linearIndependent_fin2, linearIndependent_comp_subtype_iff, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Fintype.linearIndependent_iffₛ, linearIndependent_empty_type, LinearIndependent.map_of_injective_injectiveₛ, linearIndependent_monoidHom, Pi.linearIndependent_single_of_ne_zero, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right, LinearIndependent.map_pow_expChar_pow_of_isSeparable', LinearIndependent.pair_iffₛ, Matrix.linearIndependent_cols_of_isUnit, Module.End.eigenvectors_linearIndependent, LinearIndependent.option, RootPairing.IsReduced.linearIndependent_iff, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_right, linearIndependent_zero_iff, LinearIndependent.map_of_surjective_injective, LinearIndependent.of_linearIndepOn_range, LinearIndependent.pair_neg_left_iff, linearIndependent_restrict_iff, LinearIndependent.neg, RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four, LinearIndepOn.linearIndependent, natCast_le_rank_iff, exists_linearIndependent_cons_of_lt_rank, linearIndependent_sum, linearIndependent_algHom_toLinearMap', Matrix.linearIndependent_cols_of_det_ne_zero, linearIndependent_of_subsingleton, exists_linearIndependent_pair_of_one_lt_rank, LinearIndependent.pair_smul_iff, LinearIndependent.eventually, linearIndependent_fin_cons, Module.le_rank_iff, Fintype.not_linearIndependent_iffₛ, IntermediateField.LinearDisjoint.linearIndependent_mul, linearIndependent_equiv', linearIndependent_algHom_toLinearMap, linearIndependent_toLinearMap, linearIndep_groupLikeVal, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, Matrix.linearIndependent_rows_of_isUnit, PiLp.linearIndependent_single_of_ne_zero, linearIndependent_iff', Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, LinearIndependent.map_injOn, Module.End.eigenvectors_linearIndependent', LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent, iSupIndep_iff_linearIndependent_of_ne_zero, exists_finset_linearIndependent_of_le_finrank, linearIndepOn_id_range_iff, LinearIndependent.of_isLocalized_maximal, LinearIndependent.localization_localization, LinearIndependent.of_pairwise_dual_eq_zero_one, RootPairing.EmbeddedG2.linearIndependent_short_long, exists_linearIndependent_pair_of_one_lt_finrank, RootPairing.chainTopCoeff_eq_zero_iff, Matrix.posDef_gram_iff_linearIndependent, linearIndependent_span, Module.IsLocalRing.linearIndependent_of_flat, LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm, linearIndependent_unique_iff, linearIndependent_inl_union_inr', Fintype.linearIndependent_iff'ₛ, not_linearIndependent_iffₒₛ, exists_linearIndependent, LinearIndependent.map', LinearMap.linearIndependent_iff, linearIndependent_subtype_iff, RootPairing.linearIndependent_of_add_mem_range_root, Finsupp.linearIndependent_single_of_ne_zero, RootPairing.linearIndependent_of_add_mem_range_root', LinearIndependent.tmul_of_flat_left, LinearIndependent.restrict_scalars', LinearMap.linearIndependent_iff_of_disjoint, not_linearIndependent_iffₛ, linearIndepOn_range_iff, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, linearIndependent_fin_succ', Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, RootPairing.linearIndependent_iff_coxeterWeight_ne_four, Matrix.linearIndependent_cols_iff_isUnit, Polynomial.linearIndependent_powers_iff_aeval, IsLocalizedModule.linearIndependent_lift, Submodule.exists_fun_fin_finrank_span_eq, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left, RootPairing.IsReduced.linearIndependent, LinearMap.BilinForm.linearIndependent_of_iIsOrtho, Matrix.linearIndependent_of_posDef_gram, linearIndependent_smul, Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right, Module.Flat.linearIndependent_one_tmul, linearIndependent_fin_snoc, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, linearIndependent_iff_eq_zero_of_smul_mem_span, LinearIndependent.pair_symm_iff, linearIndependent_set_iff_affineIndependent_vadd_union_singleton, IsLocalFrameOn.linearIndependent, MvPolynomial.linearIndependent_X, LinearIndependent.localization, exists_linearIndependent', LinearIndependent.iff_fractionRing, LinearIndependent.of_comp, Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left, linearIndependent_equiv, IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt, LinearIndependent.fin_cons, Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat, Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, linearIndependent_fin_succ, Profinite.NobelingProof.GoodProducts.linearIndependent, not_linearIndependent_iff_finsupp, linearIndependent_of_ne_zero_of_inner_eq_zero, LinearIndependent.pair_iff', bernsteinPolynomial.linearIndependent_aux, Module.Basis.linearIndependent_coord, exists_set_linearIndependent, Subalgebra.LinearDisjoint.linearIndependent_right_of_flat, Fintype.linearIndependent_iff, LinearIndependent.of_linearIndependent_subset, RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero, linearIndependent_iff_injective_fintypeLinearCombination, linearIndependent_algebraMap_comp_iff, Finsupp.linearIndependent_single_iff, linearIndependent_iff'', linearIndependent_add_smul_iff, iSupIndep.linearIndependent, Fintype.not_linearIndependent_iff, PiLp.linearIndependent_single, Projectivization.dependent_iff, LinearIndependent.fin_cons', Module.Basis.linearIndependent, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat, linearIndependent_iff_finset_linearIndependent, LinearIndependent.inl_union_inr, LinearIndependent.sum_smul_of_nondegenerate, IntermediateField.LinearDisjoint.linearIndependent_right, Matrix.linearIndependent_rows_of_det_ne_zero, LinearIndependent.tmul_of_isDomain, AlgebraicIndependent.linearIndependent, LinearIndependent.map_pow_expChar_pow_of_isSeparable, linearIndependent_iffₛ, LinearIndependent.of_isLocalizedModule, ModuleCat.linearIndependent_leftExact, linearIndependent_iff, crossProduct_ne_zero_iff_linearIndependent, LinearIndependent.of_subsingleton, Profinite.NobelingProof.GoodProducts.linearIndependentEmpty, sameRay_or_sameRay_neg_iff_not_linearIndependent, LinearIndependent.units_smul, LinearIndependent.pair_add_left_iff, RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent, exists_linearIndependent_algEquiv_apply, Module.Finite.not_linearIndependent_of_infinite, linearIndependent_subsingleton_iff, linearIndependent_iff_notMem_span, Subalgebra.LinearDisjoint.linearIndependent_left_of_flat_of_commute, span_flip_eq_top_iff_linearIndependent, Pi.linearIndependent_single_one, LinearMap.linearIndependent_iff_of_injOn, not_linearIndependent_iff, LinearIndependent.units_smul_iff, LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero, LinearIndependent.pair_neg_right_iff, InnerProductSpace.gramSchmidt_linearIndependent, affineIndependent_iff_linearIndependent_vsub, Finsupp.linearIndependent_single, LinearIndependent.linearIndependent_of_exact_of_retraction, linearIndependent_subsingleton_index_iff, AddChar.linearIndependent, Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial, exists_linearIndependent_snoc_of_lt_rank, Subalgebra.LinearDisjoint.linearIndependent_left_of_flat, LinearIndependent.group_smul, Matrix.mulVec_injective_iff, linearIndependent_option', linearIndependent_finset_map_embedding_subtype, IntermediateField.LinearDisjoint.linearIndependent_mul', LinearIndependent.tmul_of_flat_right, RootPairing.chainBotCoeff_eq_zero_iff, Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_right, LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat, le_rank_iff_exists_linearIndependent_finset, LinearIndependent.sumElim_of_quotient, Polynomial.Sequence.linearIndependent, PeriodPair.indep, bernsteinPolynomial.linearIndependent, linearIndependent_pow, LinearIndependent.restrict_scalars, RootPairing.GeckConstruction.linearIndependent_h, exteriorPower.ιMulti_family_linearIndependent_ofBasis, not_linearIndependent_iff_linearCombination, LinearIndependent.map_of_isPurelyInseparable_of_isSeparable, Projectivization.independent_iff, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range, LinearIndependent.of_linearIndepOn_id_range, LinearIndependent.comp, Matrix.linearIndependent_cols_of_invertible, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, Matrix.vecMul_injective_iff, NumberField.mixedEmbedding.fundamentalCone.linearIndependent_completeFamily, DFinsupp.linearIndependent_single, linearIndependent_iff''ₛ, LieAlgebra.Basis.linearIndependent_baseSupp, Profinite.NobelingProof.GoodProducts.linearIndependentSingleton, RootPairing.linearIndependent_of_sub_mem_range_root, linearIndependent_iff'ₛ, Fintype.not_linearIndependent_iffₒₛ, LinearIndependent.map, LinearMap.le_rank_iff_exists_linearIndependent_finset, Transcendental.linearIndependent_sub_inv, PiLp.linearIndependent_single_one, GeneralSchauderBasis.linearIndependent, Module.Basis.is_basis_iff_det, linearIndependent_iffₒₛ, linearIndependent_empty, isOpen_setOf_linearIndependent, Finsupp.linearIndependent_single_one, LinearIndependent.pair_add_smul_add_smul_iff, LinearIndependent.pair_add_right_iff, Matrix.linearIndependent_rows_iff_isUnit, LieAlgebra.Basis.linInd, card_linearIndependent, Submodule.LinearDisjoint.linearIndependent_mul_of_flat, IntermediateField.LinearDisjoint.linearIndependent_left, linearIndependent_iff_card_eq_finrank_span, LinearIndependent.map_of_injective_injective

---

← Back to Index