Mathlib v3 is deprecated. Go to Mathlib v4

Theorem unique_factorization_monoid.integer_of_integral

Modification history

2021-07-05 14:14
src/ring_theory/polynomial/rational_root.lean
refactor(ring_theory): turn `localization_map` into a typeclass (#8119) …
Modified unique_factorization_monoid.integer_of_integralView on Github →
2020-09-22 06:16
src/ring_theory/polynomial/rational_root.lean
refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` (#4156) …
Added unique_factorization_monoid.integer_of_integralView on Github →