Commit 2024-12-09 09:03 f064040f

View on Github →

chore(Algebra/Ring): generalize Injective.isDomain (#19768)

Estimated changes

Modified Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

Modified Mathlib/Algebra/GroupWithZero/InjSurj.lean

Modified Mathlib/Algebra/GroupWithZero/NeZero.lean

added theorem domain_nontrivial

deleted theorem pullback_nonzero

Modified Mathlib/Algebra/Order/Ring/InjSurj.lean

Modified Mathlib/Algebra/Ring/Basic.lean

modified theorem IsLeftCancelMulZero.to_noZeroDivisors

modified theorem IsRightCancelMulZero.to_noZeroDivisors

Modified Mathlib/Algebra/Ring/Hom/Basic.lean

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/RingTheory/Ideal/Prime.lean

Modified Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean