Mathlib Map

Theorems · Theorem · ring theory

MulEquiv.noZeroDivisors

∀ {A : Type u_7} (B : Type u_8) [inst : MulZeroClass A] [inst_1 : MulZeroClass B] [NoZeroDivisors B] (e : A ≃* B),
  NoZeroDivisors A

If two rings are isomorphic, and the second doesn't have zero divisors, then so does the first.

Defined in
Mathlib.Algebra.Ring.Equiv
Cited by
1 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext, Quot.sound
Assumes
MulZeroClassMulZeroClassNoZeroDivisors
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MulEquiv.noZeroDivisors_iff · cited by 0MulEquiv.noZeroDivisors_i…DFunLike.coe · cited by 62936DFunLike.coemap_zero · cited by 1614map_zeroMulEquiv · cited by 1142MulEquivmap_mul · cited by 1137map_mulNoZeroDivisors · cited by 545NoZeroDivisorsMulZeroClass · cited by 232MulZeroClassMulEquiv.injective · cited by 36MulEquiv.injectiveFunction.Injective.noZeroDivisors · cited by 8Injective.noZeroDivisorsMulEquiv.noZeroDivisorsCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.