Commit 2025-03-18 04:29 1b420225

View on Github →

chore: review of erw in Analysis/ (#23032)

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

added theorem FreeMonoid.toList_cons

added theorem FreeMonoid.toList_nil

Modified Mathlib/Analysis/Normed/Group/Hom.lean

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean