Commit 2025-06-25 21:36 25f0904b

View on Github →

chore(Data/Finsupp/Basic): split file (#26309) This PR splits off a new file Option.lean from Data/Finsupp/Basic.lean. These definitions relate to finitely-supported functions on an Option type. This split anticipates #25920 adding more definitions on this subject to this new file. This also eliminates a too-long file linter, reducing tech debt.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Data/Finsupp/Basic.lean

deleted theorem Finsupp.embDomain_some_none

deleted theorem Finsupp.embDomain_some_some

deleted theorem Finsupp.eq_option_embedding_update_none_iff

deleted def Finsupp.optionEquiv

deleted theorem Finsupp.prod_option_index

deleted def Finsupp.some

deleted theorem Finsupp.some_add

deleted theorem Finsupp.some_apply

deleted theorem Finsupp.some_embDomain_some

deleted theorem Finsupp.some_single_none

deleted theorem Finsupp.some_single_some

deleted theorem Finsupp.some_update_none

deleted theorem Finsupp.some_zero

deleted theorem Finsupp.sum_option_index_smul

Created Mathlib/Data/Finsupp/Option.lean

added theorem Finsupp.embDomain_some_none

added theorem Finsupp.embDomain_some_some

added theorem Finsupp.eq_option_embedding_update_none_iff

added def Finsupp.optionEquiv

added theorem Finsupp.prod_option_index

added def Finsupp.some

added theorem Finsupp.some_add

added theorem Finsupp.some_apply

added theorem Finsupp.some_embDomain_some

added theorem Finsupp.some_single_none

added theorem Finsupp.some_single_some

added theorem Finsupp.some_update_none

added theorem Finsupp.some_zero

added theorem Finsupp.sum_option_index_smul

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean