Theorem domain_nontrivial

Modification history

2024-12-09 09:03
Mathlib/Algebra/GroupWithZero/NeZero.lean
chore(Algebra/Ring): generalize Injective.isDomain (#19768)
Added domain_nontrivialView on Github →