Commit 2023-04-25 08:27 b237400a

View on Github →

feat: Dot product of block matrices (#3642) Match https://github.com/leanprover-community/mathlib/pull/8289 data.matrix.block@3e068ece210655b7b9a9477c3aff38a492400aa1..eba5bb3155cab51d80af00e8d7d69fa271b1302b

Estimated changes