Theorems · Theorem · number theory

Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral

∀ {ι : Type u_2} {ι' : Type u_3} (K : Type u_1) [inst : Field K] [inst_1 : DecidableEq ι] [inst_2 : DecidableEq ι']
  [inst_3 : Fintype ι] [inst_4 : Fintype ι'] [inst_5 : NumberField K] {b : Module.Basis ι ℚ K}
  {b' : Module.Basis ι' ℚ K},
  (∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)) →
    (∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)) → Algebra.discr ℚ ⇑b = Algebra.discr ℚ ⇑b'

If b and b' are ℚ-bases of a number field K such that ∀ i j, IsIntegral ℤ (b.toMatrix b' i j) and ∀ i j, IsIntegral ℤ (b'.toMatrix b i j) then discr ℚ b = discr ℚ b'.

Defined in

Mathlib.NumberTheory.NumberField.Discriminant.Defs

Cited by

1 results in Mathlib

Foundations

Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDecidableEqDecidableEqFintypeFintypeNumberField