Theorems · Theorem · commutative algebra

differentIdeal_ne_bot

∀ {A : Type u_1} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [IsIntegrallyClosed A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B] [Module.Finite A B]
  [Algebra.IsSeparable (FractionRing A) (FractionRing B)], differentIdeal A B ≠ ⊥

Defined in: Mathlib.RingTheory.DedekindDomain.Different
Cited by: 3 results in Mathlib
Foundations: Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra IsDomain IsIntegrallyClosed IsDedekindDomain Module.IsTorsionFree Module.Finite Algebra.IsSeparable

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Idealstatement · cited by 4,748
Bot.botstatement and proof · cited by 4,720
IsDomainstatement and proof · cited by 2,196
Module.Finitestatement and proof · cited by 1,032
nonZeroDivisorsstatement and proof · cited by 895
IsDedekindDomainstatement and proof · cited by 668
Module.IsTorsionFreestatement and proof · cited by 600
FractionalIdealproof · cited by 423
Algebra.IsSeparablestatement and proof · cited by 210
IsIntegrallyClosedstatement and proof · cited by 203

Cited by3

Results whose statement or proof uses this declaration.

not_dvd_differentIdeal_of_intTrace_not_memproof · cited by 1
IsDedekindDomain.differentIdeal_dvd_map_differentIdealproof · cited by 1
Submodule.traceDual_eq_span_map_traceDual_of_linearDisjointproof · cited by 0