Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 16:51 201d2c61

View on Github →

refactor(data/nat/enat): rename enat to part_enat (#15235)

find+replace enat with part_enat;
reflow long lines
add a sentence to the module docstring of data.nat.enat. I'm going to define enat := with_top nat and use it as the default implementation of "nat with top".

Estimated changes

Modified archive/imo/imo2019_q4.lean

Modified src/algebra/big_operators/enat.lean

Modified src/algebra/order/sub.lean

Modified src/algebra/squarefree.lean

Modified src/data/nat/choose/factorization.lean

Modified src/data/nat/enat.lean

deleted theorem enat.add_eq_top_iff

deleted theorem enat.add_one_le_iff_lt

deleted theorem enat.add_one_le_of_lt

deleted theorem enat.add_top

deleted theorem enat.coe_add_get

deleted theorem enat.coe_coe_hom

deleted theorem enat.coe_get

deleted def enat.coe_hom

deleted theorem enat.coe_inj

deleted theorem enat.coe_le_coe

deleted theorem enat.coe_le_iff

deleted theorem enat.coe_lt_coe

deleted theorem enat.coe_lt_iff

deleted theorem enat.coe_lt_top

deleted theorem enat.coe_ne_top

deleted theorem enat.dom_coe

deleted theorem enat.dom_of_le_coe

deleted theorem enat.dom_of_le_of_dom

deleted theorem enat.dom_of_le_some

deleted theorem enat.dom_of_lt

deleted theorem enat.dom_some

deleted theorem enat.eq_top_iff_forall_le

deleted theorem enat.eq_top_iff_forall_lt

deleted theorem enat.eq_zero_iff

deleted def enat.find

deleted theorem enat.find_dom

deleted theorem enat.find_eq_top_iff

deleted theorem enat.find_get

deleted theorem enat.find_le

deleted theorem enat.get_add

deleted theorem enat.get_coe'

deleted theorem enat.get_coe

deleted theorem enat.get_eq_iff_eq_coe

deleted theorem enat.get_eq_iff_eq_some

deleted theorem enat.get_le_get

deleted theorem enat.get_one

deleted theorem enat.get_zero

deleted theorem enat.le_coe_iff

deleted theorem enat.le_def

deleted theorem enat.le_of_lt_add_one

deleted theorem enat.lt_add_one

deleted theorem enat.lt_add_one_iff_lt

deleted theorem enat.lt_coe_iff

deleted theorem enat.lt_def

deleted theorem enat.lt_find

deleted theorem enat.lt_find_iff

deleted theorem enat.lt_wf

deleted theorem enat.ne_top_iff

deleted theorem enat.ne_top_iff_dom

deleted theorem enat.ne_top_of_lt

deleted theorem enat.ne_zero_iff

deleted theorem enat.not_dom_iff_eq_top

deleted theorem enat.not_is_max_coe

deleted theorem enat.pos_iff_one_le

deleted def enat.some

deleted theorem enat.some_eq_coe

deleted def enat.to_with_top

deleted theorem enat.to_with_top_add

deleted theorem enat.to_with_top_coe'

deleted theorem enat.to_with_top_coe

deleted theorem enat.to_with_top_le

deleted theorem enat.to_with_top_lt

deleted theorem enat.to_with_top_some

deleted theorem enat.to_with_top_top'

deleted theorem enat.to_with_top_top

deleted theorem enat.to_with_top_zero'

deleted theorem enat.to_with_top_zero

deleted theorem enat.top_add

deleted theorem enat.top_eq_none

deleted theorem enat.with_top_equiv_coe

deleted theorem enat.with_top_equiv_le

deleted theorem enat.with_top_equiv_lt

deleted theorem enat.with_top_equiv_symm_coe

deleted theorem enat.with_top_equiv_symm_le

deleted theorem enat.with_top_equiv_symm_lt

deleted theorem enat.with_top_equiv_symm_top

deleted theorem enat.with_top_equiv_symm_zero

deleted theorem enat.with_top_equiv_top

deleted theorem enat.with_top_equiv_zero

deleted def enat

added theorem part_enat.add_eq_top_iff

added theorem part_enat.add_one_le_iff_lt

added theorem part_enat.add_one_le_of_lt

added theorem part_enat.add_top

added theorem part_enat.coe_add_get

added theorem part_enat.coe_coe_hom

added theorem part_enat.coe_get

added def part_enat.coe_hom

added theorem part_enat.coe_inj

added theorem part_enat.coe_le_coe

added theorem part_enat.coe_le_iff

added theorem part_enat.coe_lt_coe

added theorem part_enat.coe_lt_iff

added theorem part_enat.coe_lt_top

added theorem part_enat.coe_ne_top

added theorem part_enat.dom_coe

added theorem part_enat.dom_of_le_coe

added theorem part_enat.dom_of_le_of_dom

added theorem part_enat.dom_of_le_some

added theorem part_enat.dom_of_lt

added theorem part_enat.dom_some

added theorem part_enat.eq_top_iff_forall_le

added theorem part_enat.eq_top_iff_forall_lt

added theorem part_enat.eq_zero_iff

added def part_enat.find

added theorem part_enat.find_dom

added theorem part_enat.find_eq_top_iff

added theorem part_enat.find_get

added theorem part_enat.find_le

added theorem part_enat.get_add

added theorem part_enat.get_coe'

added theorem part_enat.get_coe

added theorem part_enat.get_eq_iff_eq_coe

added theorem part_enat.get_eq_iff_eq_some

added theorem part_enat.get_le_get

added theorem part_enat.get_one

added theorem part_enat.get_zero

added theorem part_enat.le_coe_iff

added theorem part_enat.le_def

added theorem part_enat.le_of_lt_add_one

added theorem part_enat.lt_add_one

added theorem part_enat.lt_add_one_iff_lt

added theorem part_enat.lt_coe_iff

added theorem part_enat.lt_def

added theorem part_enat.lt_find

added theorem part_enat.lt_find_iff

added theorem part_enat.lt_wf

added theorem part_enat.ne_top_iff

added theorem part_enat.ne_top_iff_dom

added theorem part_enat.ne_top_of_lt

added theorem part_enat.ne_zero_iff

added theorem part_enat.not_dom_iff_eq_top

added theorem part_enat.not_is_max_coe

added theorem part_enat.pos_iff_one_le

added def part_enat.some

added theorem part_enat.some_eq_coe

added def part_enat.to_with_top

added theorem part_enat.to_with_top_add

added theorem part_enat.to_with_top_coe'

added theorem part_enat.to_with_top_coe

added theorem part_enat.to_with_top_le

added theorem part_enat.to_with_top_lt

added theorem part_enat.to_with_top_some

added theorem part_enat.to_with_top_top'

added theorem part_enat.to_with_top_top

added theorem part_enat.to_with_top_zero'

added theorem part_enat.to_with_top_zero

added theorem part_enat.top_add

added theorem part_enat.top_eq_none

added theorem part_enat.with_top_equiv_coe

added theorem part_enat.with_top_equiv_le

added theorem part_enat.with_top_equiv_lt

added theorem part_enat.with_top_equiv_symm_coe

added theorem part_enat.with_top_equiv_symm_le

added theorem part_enat.with_top_equiv_symm_lt

added theorem part_enat.with_top_equiv_symm_top

added theorem part_enat.with_top_equiv_symm_zero

added theorem part_enat.with_top_equiv_top

added theorem part_enat.with_top_equiv_zero

added def part_enat

Modified src/data/nat/lattice.lean

Modified src/data/nat/multiplicity.lean

Modified src/data/part.lean

Modified src/data/polynomial/div.lean

Modified src/field_theory/separable.lean

Modified src/number_theory/padics/padic_norm.lean

Modified src/number_theory/padics/padic_val.lean

Modified src/ring_theory/chain_of_divisors.lean

Modified src/ring_theory/dedekind_domain/ideal.lean

Modified src/ring_theory/discrete_valuation_ring.lean

Modified src/ring_theory/multiplicity.lean

modified theorem multiplicity.dvd_iff_multiplicity_pos

modified theorem multiplicity.dvd_of_multiplicity_pos

modified theorem multiplicity.pow_dvd_of_le_multiplicity

modified def multiplicity

Modified src/ring_theory/power_series/basic.lean

modified theorem power_series.le_order

modified def power_series.order

modified theorem power_series.order_eq

Modified src/ring_theory/roots_of_unity.lean

Modified src/ring_theory/unique_factorization_domain.lean

Modified src/ring_theory/witt_vector/frobenius.lean

Modified src/set_theory/cardinal/basic.lean

deleted theorem cardinal.aleph_0_to_enat

added theorem cardinal.aleph_0_to_part_enat

deleted theorem cardinal.mk_to_enat_eq_coe_card

deleted theorem cardinal.mk_to_enat_of_infinite

added theorem cardinal.mk_to_part_enat_eq_coe_card

added theorem cardinal.mk_to_part_enat_of_infinite

deleted def cardinal.to_enat

deleted theorem cardinal.to_enat_apply_of_aleph_0_le

deleted theorem cardinal.to_enat_apply_of_lt_aleph_0

deleted theorem cardinal.to_enat_cast

deleted theorem cardinal.to_enat_surjective

added def cardinal.to_part_enat

added theorem cardinal.to_part_enat_apply_of_aleph_0_le

added theorem cardinal.to_part_enat_apply_of_lt_aleph_0

added theorem cardinal.to_part_enat_cast

added theorem cardinal.to_part_enat_surjective

Modified src/set_theory/cardinal/continuum.lean

deleted theorem cardinal.continuum_to_enat

added theorem cardinal.continuum_to_part_enat

Modified src/set_theory/cardinal/finite.lean

deleted def enat.card

deleted theorem enat.card_eq_coe_fintype_card

deleted theorem enat.card_eq_top_of_infinite

added def part_enat.card

added theorem part_enat.card_eq_coe_fintype_card

added theorem part_enat.card_eq_top_of_infinite

Modified src/set_theory/cardinal/ordinal.lean

deleted theorem cardinal.aleph_to_enat

added theorem cardinal.aleph_to_part_enat