theorem discr_smul_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (c : K) (b : Fin (Module.finrank K L) → L) : (Algebra.discr K fun (i : Fin (Module.finrank K L)) => c • b i) = c ^ (2 * Module.finrank K L) * Algebra.discr K b

theorem imageOfB_subset_imageOfSB (A : Type u_1) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [Algebra A L] [IsScalarTower A B L] [IsDomain A] [IsIntegrallyClosed A] [IsIntegralClosure B A L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (SA : Type u_5) [CommRing SA] [IsDomain SA] [Algebra A SA] (SB : Type u_6) [CommRing SB] [IsDomain SB] [Algebra B SB] [Algebra SA SB] [Algebra A SB] [Algebra SA L] [Algebra SB L] [IsScalarTower A SA SB] [IsScalarTower A B SB] [IsScalarTower A SA L] [IsScalarTower SA SB L] [IsIntegrallyClosed SA] [IsFractionRing SB L] [IsDedekindDomain SB] [Module.IsTorsionFree SA SB] [Module.IsTorsionFree B SB] [IsIntegralClosure SB SA L] [Nontrivial SB] [NoZeroDivisors SB] [IsScalarTower B SB L] : ↑(imageOfB A L B) ⊆ ↑(imageOfB SA L SB)

theorem latticeDiscrSet_B_subset_SB (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (SA : Type u_5) [CommRing SA] [IsDomain SA] [Algebra A SA] (SB : Type u_6) [CommRing SB] [IsDomain SB] [Algebra B SB] [Algebra SA SB] [Algebra A SB] [Algebra SA L] [Algebra SA K] [Algebra SB L] [IsScalarTower A SA SB] [IsScalarTower A B SB] [IsScalarTower A SA L] [IsScalarTower A SA K] [IsScalarTower SA SB L] [IsScalarTower SA K L] [IsFractionRing SA K] [IsIntegrallyClosed SA] [IsFractionRing SB L] [IsDedekindDomain SB] [Module.IsTorsionFree SA SB] [Module.IsTorsionFree B SB] [IsIntegralClosure SB SA L] [Nontrivial SB] [NoZeroDivisors SB] [IsScalarTower B SB L] : latticeDiscrSet A K (imageOfB A L B) ⊆ latticeDiscrSet SA K (imageOfB SA L SB)

theorem proposition_12_15 (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) (SA : Type u_5) [CommRing SA] [IsDomain SA] [Algebra A SA] [IsLocalization S SA] (SB : Type u_6) [CommRing SB] [IsDomain SB] [Algebra B SB] [IsLocalization (Algebra.algebraMapSubmonoid B S) SB] [Algebra SA SB] [Algebra A SB] [Algebra SA L] [Algebra SA K] [Algebra SB L] [IsScalarTower A SA SB] [IsScalarTower A B SB] [IsScalarTower A SA L] [IsScalarTower A SA K] [IsScalarTower SA SB L] [IsScalarTower SA K L] [IsFractionRing SA K] [IsIntegrallyClosed SA] [IsFractionRing SB L] [IsDedekindDomain SB] [Module.IsTorsionFree SA SB] [Module.IsTorsionFree B SB] [IsIntegralClosure SB SA L] [Nontrivial SB] [NoZeroDivisors SB] [IsScalarTower B SB L] : Submodule.span SA ↑(extensionDiscriminant A K L B) = extensionDiscriminant SA K L SB