Commit 2023-04-17 07:18 4fe63cb5

View on Github →

chore: tidy various files (#3474)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Over.lean

Modified Mathlib/Data/Real/Pointwise.lean

Modified Mathlib/GroupTheory/FreeGroup.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Modified Mathlib/ModelTheory/LanguageMap.lean

Modified Mathlib/Order/Filter/Pointwise.lean

modified def Filter.mapMonoidHom

deleted theorem Filter.nsmul_top

Modified Mathlib/Topology/Algebra/Group/Basic.lean

modified def Units.Homeomorph.prodUnits

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/List.lean

added theorem List.tendsto_insertNth'

deleted theorem List.tendsto_insert_nth'

added theorem Vector.continuous_insertNth'

deleted theorem Vector.continuous_insert_nth'

Modified Mathlib/Topology/Separation.lean