mathlib
a1b35592 - chore(algebra/order/ring/canonical): use implicit variables (#18167)

Commit
3 years ago
chore(algebra/order/ring/canonical): use implicit variables (#18167) Make implicitness of variables for `eq_zero_or_eq_zero_of_mul_eq_zero` consistent in `canonically_ordered_comm_semiring` and `no_zero_divisors_`. See the discussion in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Data.2ESet.2ESemiring Corresponds to [#1545](https://github.com/leanprover-community/mathlib4/pull/1545).
Parents
Loading