Commit 2023-10-22 10:07 004800e4

View on Github →

refactor: List.All₂ to List.Forall (#7797) This renames List.All₂ to List.Forall, because the ₂ is highly confusing when it usually means “two lists”, and we had users on Zulip not find List.Forall because of that (https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Is.20there.20List.2EForall.E2.82.82.2C.20but.20for.20one.20list.3F.20.28In.20library.20Std.29/near/397551365)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.All₂.imp

added theorem List.Forall.imp

deleted theorem List.all₂_cons

deleted theorem List.all₂_iff_forall

deleted theorem List.all₂_map_iff

added theorem List.forall_cons

added theorem List.forall_iff_forall_mem

added theorem List.forall_map_iff

Modified Mathlib/Data/List/Defs.lean

deleted def List.All₂

added def List.Forall

Modified Mathlib/Data/List/Zip.lean

deleted theorem List.all₂_zipWith

added theorem List.forall_zipWith

Modified Mathlib/NumberTheory/Dioph.lean

deleted theorem Dioph.DiophList.all₂

added theorem Dioph.DiophList.forall

modified theorem Dioph.inter

modified theorem Poly.sumsq_eq_zero

Modified Mathlib/Topology/MetricSpace/MetrizableUniformity.lean