Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 23:45 a7611b2c

View on Github →

chore(*): notation for units (#11236)

Estimated changes

modified theorem units_int.one_ne_neg_one
modified def with_sign
modified theorem spectrum.smul_mem_smul_iff
modified theorem spectrum.unit_smul_eq_smul
modified def associated
modified theorem associates.coe_unit_eq_one
modified theorem associates.units_eq_one
modified theorem unit_associated_one
modified theorem units_eq_one
modified theorem units.coe_prod
modified theorem ring_hom.map_units_inv
modified theorem exists_eq_pow_of_mul_eq_pow
modified theorem lcm_units_coe_left
modified theorem lcm_units_coe_right
modified theorem normalize_coe_units
modified def is_conj
modified theorem units.coe_op_equiv_symm
modified theorem units.coe_unop_op_equiv
modified def units.op_equiv
modified def embed_product
modified def mul_equiv.prod_units
modified theorem semiconj_by.units_coe
modified theorem semiconj_by.units_coe_iff
modified theorem semiconj_by.units_inv_right
modified theorem semiconj_by.units_of_coe
modified theorem units.mk_semiconj_by
modified def divp
modified theorem divp_assoc
modified theorem divp_divp_eq_divp_mul
modified theorem divp_eq_divp_iff
modified theorem divp_eq_iff_mul_eq
modified theorem divp_eq_one_iff_eq
modified theorem divp_inv
modified theorem divp_left_inj
modified theorem divp_mul_cancel
modified theorem divp_mul_divp
modified theorem divp_self
modified def is_unit
modified theorem mul_divp_cancel
modified theorem one_divp
modified theorem units.coe_eq_one
modified theorem units.coe_one
modified def units.copy
modified theorem units.copy_eq
modified theorem units.eq_iff
modified theorem units.ext_iff
modified theorem units.inv_eq_coe_inv
modified theorem units.inv_eq_of_mul_eq_one
modified theorem units.inv_mul_cancel_left
modified theorem units.inv_mul_cancel_right
modified theorem units.inv_mul_of_eq
modified theorem units.inv_unique
modified theorem units.is_unit_mul_units
modified theorem units.is_unit_units_mul
modified theorem units.mk_coe
modified theorem units.mul_inv_cancel_left
modified theorem units.mul_inv_cancel_right
modified theorem units.mul_inv_of_eq
modified theorem units.mul_left_inj
modified theorem units.mul_right_inj
modified def units.simps.coe
modified def units.simps.coe_inv
modified def units.coe_hom
modified theorem units.coe_hom_apply
modified theorem units.coe_lift_right
modified theorem units.coe_map
modified theorem units.coe_map_inv
modified def units.lift_right
modified theorem units.lift_right_inv_mul
modified def units.map
modified theorem units.map_id
modified theorem units.mul_lift_right_inv
modified theorem commute.units_zpow_left
modified theorem commute.units_zpow_right
modified theorem int.units_sq
modified theorem units.coe_pow
modified theorem units.coe_zpow
modified theorem units.conj_pow'
modified theorem units.conj_pow
modified theorem divp_eq_div
modified theorem ring.inverse_unit
modified theorem units.coe_inv'
modified theorem units.exists_iff_ne_zero
modified theorem units.inv_mul'
modified def units.mk0
modified theorem units.mk0_coe
modified theorem units.mul_inv'
modified theorem units.mul_left_eq_zero
modified theorem units.mul_right_eq_zero
modified theorem units.ne_zero
modified theorem units.coe_zpow₀
modified theorem inv_of_units
modified def unit_of_invertible
modified def units.invertible
modified theorem units.neg_smul
modified theorem units.coe_le_coe
modified theorem units.coe_lt_coe
modified theorem units.max_coe
modified theorem units.min_coe
modified theorem units.inv_neg
modified theorem units.inv_pos
modified theorem units.zero_lt
modified theorem units.is_regular
modified theorem units.is_smul_regular
modified theorem units.inv_eq_self_iff
modified theorem units.coe_star
modified theorem units.coe_star_inv
modified theorem differentiable_at_inverse
modified theorem fderiv_inverse
modified theorem has_fderiv_at_ring_inverse
modified theorem units.norm_pos
modified theorem int.nnnorm_coe_units
modified theorem int.norm_coe_units
modified theorem normed_ring.inverse_add
modified def units.add
modified theorem units.is_open_map_coe
modified def units.one_sub
modified theorem units.open_embedding_coe
modified def units.unit_of_nearby
modified def units.to_Aut
modified theorem units.to_Aut_hom
modified theorem units.to_Aut_inv
modified def to_units
modified theorem units.coe_inv
modified def units.map_equiv
modified def units.mul_left
modified theorem units.mul_left_bijective
modified theorem units.mul_left_symm
modified def units.mul_right
modified theorem units.mul_right_bijective
modified theorem units.mul_right_symm
modified theorem fintype.card_units
modified theorem fintype.card_units_int
modified def units_equiv_ne_zero
modified theorem units_int.univ
modified theorem int.units_coe_mul_self
modified theorem int.units_eq_one_or
modified theorem int.units_inv_eq_self
modified theorem int.units_mul_self
modified theorem int.units_nat_abs
modified theorem matrix.rank_unit
modified theorem nat.units_eq_one
modified theorem nat.prime_iff_card_units
modified theorem zmod.card_units_eq_totient
modified theorem polynomial.coeff_inv_units
modified theorem polynomial.degree_coe_units
modified theorem zmod.inv_coe_unit
modified def zmod.unit_of_coprime
modified theorem zmod.val_coe_unit_coprime
modified theorem units.coe_is_monoid_hom
modified theorem units.coe_map'
modified def units.map'
modified theorem circle_deg1_lift.units_coe
modified theorem finite_field.sum_pow_units
modified theorem zmod.card_units
modified theorem zmod.pow_totient
modified theorem units.chart_at_apply
modified theorem units.chart_at_source
modified theorem units.smul_def
modified theorem order_of_units
modified def equiv.perm.sign
modified def equiv.perm.sign_aux2
modified def equiv.perm.sign_aux3
modified def equiv.perm.sign_aux
modified theorem equiv.perm.sign_surjective
modified theorem submonoid.unit_mem_left_inv
modified def basis.units_smul
modified theorem basis.units_smul_apply
modified theorem basis.det_units_smul
modified theorem basis.to_matrix_units_smul
modified theorem matrix.det_units_conj'
modified theorem matrix.det_units_conj
modified theorem matrix.inv_smul'
modified theorem matrix.units.coe_inv''
modified theorem matrix.units.coe_zpow
modified theorem units_inv_smul
modified theorem units_smul_eq_neg_iff
modified theorem units_smul_eq_self_iff
modified theorem linear_map.trace_conj
modified theorem lucas_lehmer.X.units_card
modified def padic_int.mk_units
modified theorem padic_int.norm_units
modified def padic_int.unit_coeff
modified theorem zmod.euler_criterion_units
modified def class_group
modified theorem coe_to_principal_ideal
modified def to_principal_ideal
modified theorem to_principal_ideal_eq_iff
modified theorem fractional_ideal.fg_unit
modified theorem multiplicity.unit_left
modified theorem multiplicity.unit_right
modified theorem map_roots_of_unity
modified theorem mem_roots_of_unity
modified def roots_of_unity
modified theorem mem_pos_monoid
modified theorem add_valuation.map_units_inv
modified theorem valuation.map_units_inv
modified theorem valuation.unit_map_eq
modified theorem units.continuous_coe
modified theorem valued.subgroups_basis