Commit 2025-04-28 02:20 9120e17b

View on Github →

chore(*): use the preferred spelling for ne (#24408)

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Order.lean

added theorem MeromorphicAt.order_add_of_order_ne

deleted theorem MeromorphicAt.order_add_of_unequal_order

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one

deleted theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_neq_getVert_add_one

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.eq_one_of_ne_zero

deleted theorem Fin.eq_one_of_neq_zero

Modified Mathlib/Data/List/Sigma.lean

added theorem List.ne_key

deleted theorem List.not_eq_key

Modified Mathlib/LinearAlgebra/Projectivization/Independence.lean

added theorem Projectivization.independent_pair_iff_ne

deleted theorem Projectivization.independent_pair_iff_neq