Commit 2023-10-02 07:53 89df0a5a

View on Github →

chore: golf some Nat.Prime proofs (#7452) Also correct indentation for another.

Estimated changes

Modified Mathlib/Data/Nat/Prime.lean

modified theorem Nat.Prime.dvd_of_dvd_pow

modified theorem Nat.Prime.pow_not_prime'

modified theorem Nat.Prime.pow_not_prime