Theorem LinearMap.compl₁₂_id_id

Modification history

2025-06-27 14:36

Mathlib/LinearAlgebra/BilinearMap.lean

fix: generalize `CommSemiring` to `Semiring` for bilinear map composition (#26458) …

Modified LinearMap.compl₁₂_id_id View on Github →

2023-02-28 06:48

Mathlib/LinearAlgebra/BilinearMap.lean

feat: port LinearAlgebra.BilinearMap (#2434)

Added LinearMap.compl₁₂_id_id View on Github →