Multiplicity of a divisor #
For a commutative monoid, this file introduces the notion of multiplicity of a divisor and proves several basic results on it.
Main definitions #
emultiplicity a b
: for two elementsa
andb
of a commutative monoid returns the largest numbern
such thata ^ n ∣ b
or infinity, written⊤
, ifa ^ n ∣ b
for all natural numbersn
.multiplicity a b
: aℕ
-valued version ofmultiplicity
, defaulting for1
instead of⊤
. The reason for using1
as a default value instead of0
is to havemultiplicity_eq_zero_iff
.FiniteMultiplicity a b
: a predicate denoting that the multiplicity ofa
inb
is finite.
multiplicity.Finite a b
indicates that the multiplicity of a
in b
is finite.
Instances For
Alias of FiniteMultiplicity
.
multiplicity.Finite a b
indicates that the multiplicity of a
in b
is finite.
Equations
Instances For
emultiplicity a b
returns the largest natural number n
such that
a ^ n ∣ b
, as an ℕ∞
. If ∀ n, a ^ n ∣ b
then it returns ⊤
.
Equations
- emultiplicity a b = if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤
Instances For
A ℕ
-valued version of emultiplicity
, returning 1
instead of ⊤
.
Equations
- multiplicity a b = WithTop.untop' 1 (emultiplicity a b)
Instances For
Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top
.
Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top
.
Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top
.
Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top
.
Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top
.
Alias of FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq
.
Alias of FiniteMultiplicity.emultiplicity_le_of_multiplicity_le
.
Alias of FiniteMultiplicity.le_multiplicity_of_le_emultiplicity
.
Alias of FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt
.
Alias of FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity
.
Alias of FiniteMultiplicity.def
.
Alias of FiniteMultiplicity.not_dvd_of_one_right
.
Alias of Int.natCast_multiplicity
.
Alias of FiniteMultiplicity.not_iff_forall
.
Alias of FiniteMultiplicity.not_unit
.
Alias of FiniteMultiplicity.mul_left
.
Alias of FiniteMultiplicity.multiplicity_eq_iff
.
Alias of FiniteMultiplicity.not_of_isUnit_left
.
Alias of FiniteMultiplicity.not_of_one_left
.
Alias of FiniteMultiplicity.one_right
.
Alias of FiniteMultiplicity.not_of_unit_left
.
Alias of FiniteMultiplicity.multiplicity_le_multiplicity_iff
.
Alias of Nat.finiteMultiplicity_iff
.
Alias of the reverse direction of dvd_iff_multiplicity_pos
.
Alias of FiniteMultiplicity.mul_right
.
Alias of FiniteMultiplicity.ne_zero
.
Alias of FiniteMultiplicity.or_of_add
.
Alias of FiniteMultiplicity.neg_iff
.
Alias of the reverse direction of FiniteMultiplicity.neg_iff
.
Alias of the reverse direction of FiniteMultiplicity.neg_iff
.
Alias of the reverse direction of FiniteMultiplicity.neg_iff
.
Alias of Prime.finiteMultiplicity_mul
.
Alias of FiniteMultiplicity.mul_iff
.
Alias of FiniteMultiplicity.pow
.
Alias of FiniteMultiplicity.emultiplicity_self
.
Alias of FiniteMultiplicity.multiplicity_pow
.
Alias of Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs
.
Alias of Int.finiteMultiplicity_iff
.
Equations
- x✝¹.decidableFiniteMultiplicity x✝ = decidable_of_iff' (x✝¹ ≠ 1 ∧ 0 < x✝) ⋯
Alias of Nat.decidableFiniteMultiplicity
.
Instances For
Equations
- x✝¹.decidableMultiplicityFinite x✝ = decidable_of_iff' (x✝¹.natAbs ≠ 1 ∧ x✝ ≠ 0) ⋯
Alias of Int.decidableMultiplicityFinite
.