mathlib
825edd3c - chore(ring_theory): protect `algebra.is_integral` (#18178)

Commit

2 years ago

chore(ring_theory): protect `algebra.is_integral` (#18178) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author

alreadydone

Parents