Commit 2024-08-07 05:28 53f5571e

View on Github →

chore: backports for leanprover/lean4#4814 (part 17) (#15429) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

modified theorem QuaternionAlgebra.coe_smul
modified theorem QuaternionAlgebra.smul_im
modified theorem Algebra.adjoin_top
modified theorem OrthogonalIdempotents.map
modified theorem Associates.count_mul
modified theorem Associates.count_of_coprime
modified theorem Associates.count_pow
modified theorem Associates.count_self
modified theorem Associates.dvd_count_pow