Mathlib Map

Theorems · Theorem · number theory

NumberField.Ideal.primesOverSpanEquivMonicFactorsMod.congr_simp

∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ),
  NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp = NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp
Defined in
Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Cited by
0 results in Mathlib
Foundations
Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldFactNumberField
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set · cited by 53352SetFinset · cited by 13712FinsetEquiv · cited by 8337EquivField · cited by 7404FieldSet.Elem · cited by 7166Set.ElemPolynomial · cited by 5681PolynomialIdeal · cited by 4748IdealFact · cited by 2726FactNat.Prime · cited by 2059Nat.PrimeZMod · cited by 1024ZModIdeal.span · cited by 948Ideal.spanNumberField · cited by 653NumberFieldNumberField.RingOfIntegers · cited by 413NumberField.RingOfIntegersIdeal.primesOver · cited by 84Ideal.primesOverRingOfIntegers.exponent · cited by 15RingOfIntegers.exponentprimesOverSpanEquivMonicFacto…CITED BYCITES

Cites17

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

  • Setstatement · cited by 53,352
  • Finsetstatement · cited by 13,712
  • Equivstatement · cited by 8,337
  • Fieldstatement and proof · cited by 7,404
  • Set.Elemstatement · cited by 7,166
  • Polynomialstatement · cited by 5,681
  • Idealstatement · cited by 4,748
  • Factstatement and proof · cited by 2,726
  • Nat.Primestatement and proof · cited by 2,059
  • ZModstatement · cited by 1,024
  • Ideal.spanstatement · cited by 948
  • NumberFieldstatement and proof · cited by 653

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.