Commit 2023-03-27 13:58 5fddd0c6

View on Github →

chore: forward-port leanprover-community/mathlib#18644 (#3121)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/MStructure.lean

Modified Mathlib/Data/List/Func.lean

modified theorem List.Func.nil_sub

modified theorem List.Func.sub_nil

Modified Mathlib/Logic/Equiv/List.lean

modified def Equiv.listEquivSelfOfEquivNat