Commit 2026-05-19 08:05 ae225e96

chore(LinearAlgebra/SesquilinearForm): generalize orthogonalBilin in order to simplify definition of orthogonal (#37389)

• generalize Submodule.orthogonalBilin to CommSemiring and AddCommMonoid, and to general sesquilinear forms with inputs from different modules. This enables subsequent changes.
• redefine BilinForm.orthogonal in terms of orthogonalBilin.
• reorder arguments of Submodule.orthogonalBilin to match other instances of duality across mathlib.

For comparison Before

Submodule.orthogonalBilin.{u_1, u_2, u_5, u_6} {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6}
  [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] [AddCommGroup M] [Module R M] {I₁ I₂ : R₁ →+* R}
  (N : Submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) : Submodule R₁ M₁

After

Submodule.orthogonalBilin.{u_1, u_2, u_3, u_5, u_6, u_7} {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5}
  {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M] [Module R M]
  [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M)
  (N : Submodule R₁ M₁) : Submodule R₂ M₂

A few fixes in other files have been necessary as well. This is an extract from #37381.