Commit 2025-08-29 03:39 840619d6

View on Github →

chore(Data): process porting notes (#28975) Deal with a few porting notes in the Data folder. Also a couple style fixes that I noticed while going through everything.

Estimated changes

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/List/Defs.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Permutation.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/NNReal/Defs.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Option/NAry.lean

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/Data/Seq/Basic.lean

modified theorem Stream'.Seq.head_eq_destruct

Modified Mathlib/Data/Vector/Basic.lean