def BilinPairing.IsSymmetric (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] (B : M →ₗ[A] M →ₗ[A] A) : Prop

def BilinPairing.inducedMap (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] (B : M →ₗ[A] M →ₗ[A] A) : M →ₗ[A] Module.Dual A M

@[reducible, inline]

abbrev IsPerfectSelfPairing (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] (p : M →ₗ[A] M →ₗ[A] A) : Prop

structure IsALattice (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (M : Submodule A V) : Prop

• fg : M.FG
• span_eq_top : Submodule.span K ↑M = ⊤

def dualLattice (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (φ : V →ₗ[K] V →ₗ[K] K) (M : Submodule A V) : Submodule A V