Mathlib Map

Theorems · Theorem · number theory

NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ}
  (a : { a // NumberField.mixedEmbedding.norm ↑a = ↑n }),
  ↑↑((NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm K n) a).1 =
    Ideal.span {↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet ↑a)}
Defined in
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Cited by
0 results in Mathlib
Foundations
Depth 341 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldNumberField
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetReal · cited by 25697RealEquiv · cited by 8337EquivField · cited by 7404FieldSet.Elem · cited by 7166Set.ElemComplex · cited by 5565ComplexIdeal · cited by 4748IdealEquiv.symm · cited by 3681Equiv.symmSubgroup · cited by 3593SubgroupSubmonoid · cited by 3086SubmonoidUnits · cited by 2804UnitsIdeal.span · cited by 948Ideal.spannonZeroDivisors · cited by 895nonZeroDivisorsMonoidWithZeroHom · cited by 704MonoidWithZeroHomfundamentalCone.integerSetEqu…CITED BYCITES

Cites32

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

  • DFunLike.coestatement and proof · cited by 62,936
  • Setstatement · cited by 53,352
  • Realstatement · cited by 25,697
  • Equivstatement · cited by 8,337
  • Fieldstatement and proof · cited by 7,404
  • Set.Elemstatement and proof · cited by 7,166
  • Complexstatement · cited by 5,565
  • Idealstatement and proof · cited by 4,748
  • Equiv.symmproof · cited by 3,681
  • Subgroupstatement · cited by 3,593
  • Submonoidstatement · cited by 3,086
  • Unitsstatement and proof · cited by 2,804

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.