Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-09 09:32 c9bcaa7b

View on Github →

chore(*): remove some local attribute [semireducible]s (#17874)

Estimated changes

Modified counterexamples/char_p_zero_ne_char_zero.lean

modified theorem add_one_eq_one

Modified src/data/int/range.lean

Modified src/data/nat/modeq.lean

Modified src/ring_theory/localization/fraction_ring.lean

Modified src/topology/constructions.lean

modified theorem nhds_of_add

modified theorem nhds_of_dual

modified theorem nhds_of_mul

modified theorem nhds_to_add

modified theorem nhds_to_dual

modified theorem nhds_to_mul