Theorems · Definition · number theory
NumberField.RingOfIntegers.basis
(K : Type u_1) →
[inst : Field K] →
[inst_1 : NumberField K] →
Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℤ (NumberField.RingOfIntegers K)A ℤ-basis of the ring of integers of K.
- Defined in
- Mathlib.NumberTheory.NumberField.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldNumberField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- Module.Basisstatement · cited by 1,477
- NumberFieldstatement and proof · cited by 653
- NumberField.RingOfIntegersstatement and proof · cited by 413
- Module.Free.ChooseBasisIndexstatement · cited by 133
- Module.Free.chooseBasisproof · cited by 121
Cited by14
Results whose statement or proof uses this declaration.
- NumberField.discrproof · cited by 53
- NumberField.integralBasisproof · cited by 25
- NumberField.canonicalEmbedding.latticeBasis_applyproof · cited by 7
- NumberField.integralBasis_applystatement and proof · cited by 6
- NumberField.absNorm_differentIdealproof · cited by 4
- NumberField.coe_discrproof · cited by 4
- NumberField.mixedEmbedding.latticeBasis_applyproof · cited by 4
- NumberField.mem_span_integralBasisproof · cited by 3
- NumberField.discr_eq_discrproof · cited by 3
- NumberField.basisMatrix_eq_embeddingsMatrixReindexproof · cited by 2
- NumberField.conj_basisMatrixproof · cited by 1
- NumberField.det_basisOfFractionalIdeal_eq_absNormproof · cited by 1