Commit 2023-01-18 16:31 7092d7ca

View on Github →

feat port: RingTheory.Prime (#1646)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Prime.lean

added theorem Prime.abs

added theorem Prime.neg

added theorem mul_eq_mul_prime_pow

added theorem mul_eq_mul_prime_prod