theorem dual_map_apply {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (φ : M →ₗ[A] N) (g : Module.Dual A N) (m : M) : (φ.dualMap g) m = g (φ m)

def dualDirectSumEquiv (A : Type u_1) [CommRing A] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] : Module.Dual A (M × N) ≃ₗ[A] Module.Dual A M × Module.Dual A N

def colonSubmodule (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (M : Submodule A K) : Submodule A K

noncomputable def colonToA (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (M : Submodule A K) (x : ↥(colonSubmodule A K M)) (m : ↥M) : A

theorem colonToA_spec (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (M : Submodule A K) (x : ↥(colonSubmodule A K M)) (m : ↥M) : (algebraMap A K) (colonToA A K M x m) = ↑x * ↑m

noncomputable def colonToDualMap (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) : ↥(colonSubmodule A K M) →ₗ[A] Module.Dual A ↥M

theorem dual_symmetric_relation (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) (f : Module.Dual A ↥M) (m₁ m₂ : ↥M) : ↑m₁ * (algebraMap A K) (f m₂) = ↑m₂ * (algebraMap A K) (f m₁)

theorem dual_apply_via_element (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) (f : Module.Dual A ↥M) (m₀ : ↥M) (hm₀ : ↑m₀ ≠ 0) (m : ↥M) : (algebraMap A K) (f m₀) * (↑m₀)⁻¹ * ↑m = (algebraMap A K) (f m)

noncomputable def dualToColonMap (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) (m₀ : ↥M) (hm₀ : ↑m₀ ≠ 0) : Module.Dual A ↥M →ₗ[A] ↥(colonSubmodule A K M)

noncomputable def dualEquivColonSubmodule (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) (m₀ : ↥M) (hm₀ : ↑m₀ ≠ 0) : Module.Dual A ↥M ≃ₗ[A] ↥(colonSubmodule A K M)

theorem colonSubmodule_eq_coe_inv (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : FractionalIdeal (nonZeroDivisors A) K) (hM : M ≠ 0) : colonSubmodule A K ↑M = ↑M⁻¹

noncomputable def nonzeroElemOfFractionalIdeal (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : FractionalIdeal (nonZeroDivisors A) K) (hM : M ≠ 0) : { m : ↥↑M // ↑m ≠ 0 }

noncomputable def dualEquivInverse (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : FractionalIdeal (nonZeroDivisors A) K) (hM : IsUnit M) : Module.Dual A ↥↑M ≃ₗ[A] ↥↑M⁻¹

noncomputable def doubleDualEquiv (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : FractionalIdeal (nonZeroDivisors A) K) (hM : IsUnit M) : Module.Dual A (Module.Dual A ↥↑M) ≃ₗ[A] ↥↑M

theorem dualBasisProperty {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] [Finite ι] (b : Module.Basis ι A M) (i j : ι) : (b.dualBasis i) (b j) = if j = i then 1 else 0

noncomputable def perfPairingDualBasis {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] [Finite ι] (p : M →ₗ[A] M →ₗ[A] A) [p.IsPerfPair] (b : Module.Basis ι A M) : Module.Basis ι A M

theorem prime_chain_contracts_of_integral {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] {q₀ q₁ : Ideal B} [q₀.IsPrime] (hlt : q₀ < q₁) : Ideal.comap (algebraMap A B) q₀ < Ideal.comap (algebraMap A B) q₁

theorem integral_closure_isDedekindDomain (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsDomain C] [IsDedekindDomain A] : IsDedekindDomain C

theorem ringOfIntegers_isDedekindDomain (K : Type u_1) [Field K] [NumberField K] : IsDedekindDomain (NumberField.RingOfIntegers K)