Commit 2023-01-30 00:50 d4732581

View on Github →

feat: Port Algebra.IsPrimePow (#1925)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/IsPrimePow.lean

added theorem IsPrimePow.dvd

added theorem IsPrimePow.ne_one

added theorem IsPrimePow.ne_zero

added theorem IsPrimePow.not_unit

added theorem IsPrimePow.one_lt

added theorem IsPrimePow.pos

added theorem IsPrimePow.pow

added theorem IsPrimePow.two_le

added def IsPrimePow

added theorem IsUnit.not_isPrimePow

added theorem Nat.Prime.isPrimePow

added theorem Nat.disjoint_divisors_filter_isPrimePow

added theorem Prime.isPrimePow

added theorem isPrimePow_def

added theorem isPrimePow_iff_pow_succ

added theorem isPrimePow_nat_iff

added theorem isPrimePow_nat_iff_bounded

added theorem not_isPrimePow_one

added theorem not_isPrimePow_zero