prime) factors of a prime number is the list [p] (#2452)

Commit

5 years ago

feat(data/nat/prime) factors of a prime number is the list [p] (#2452) The factors of a prime number are [p]. Co-authored-by: Scott Morrison <scott@tqft.net>

References

#2700 - Fix merge conflict

Author

alexjbest

Parents

99245b33

mathlib3 0ceac44d - feat(data/nat/prime) factors of a prime number is the list [p] (#2452)

mathlib3
0ceac44d - feat(data/nat/prime) factors of a prime number is the list [p] (#2452)