Commit 2025-01-06 07:44 9afdff78

View on Github →

chore(LinearIndependent): generalize to semirings (#20480) After the definition is changed in #18426, many results can now be generalized to semirings.

Estimated changes

Modified Mathlib/Data/Finsupp/Basic.lean

modified def Finsupp.restrictSupportEquiv

added theorem Finsupp.subtypeDomain_eq_iff

added theorem Finsupp.subtypeDomain_eq_iff_forall

modified theorem Finsupp.subtypeDomain_eq_zero_iff'

Modified Mathlib/Data/Set/Function.lean

added theorem Set.InjOn.injective_iff

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added theorem Finsupp.linearCombination_restrict

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

modified def Finsupp.supportedEquivFinsupp

added theorem Finsupp.supportedEquivFinsupp_symm_apply_coe

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem Fintype.linearIndependent_iff'ₛ

added theorem Fintype.linearIndependent_iff_injective

added theorem Fintype.linearIndependent_iffₛ

added theorem Fintype.not_linearIndependent_iffₛ

modified def LinearIndependent.Maximal

modified theorem LinearIndependent.eq_of_smul_apply_eq_smul_apply

added theorem LinearIndependent.image_subtypeₛ

added theorem LinearIndependent.map_injOn

modified theorem LinearIndependent.map_of_injective_injective

added theorem LinearIndependent.map_of_injective_injectiveₛ

modified theorem LinearIndependent.maximal_iff

modified theorem LinearIndependent.mono

added theorem LinearIndependent.not_smul_mem_span

added theorem LinearIndependent.pair_iffₛ

added theorem linearDependent_comp_subtype'ₛ

added theorem linearDependent_comp_subtypeₛ

added theorem linearIndependent_comp_subtypeₛ

added theorem linearIndependent_iff''ₛ

added theorem linearIndependent_iff'ₛ

added theorem linearIndependent_iff_linearCombinationOnₛ

added theorem linearIndependent_iffₛ

modified theorem linearIndependent_inl_union_inr'

added theorem linearIndependent_restrict_iff

added theorem linearIndependent_subtypeₛ

added theorem not_linearIndependent_iffₛ