Theorem Quaternion.coe_normSq_add

Modification history

2023-11-16 19:44
Mathlib/Algebra/Quaternion.lean
style: cleanup by putting `by` on the same line as `:=` (#8407)
Modified Quaternion.coe_normSq_addView on Github →
2023-11-15 21:24
Mathlib/Algebra/Quaternion.lean
perf(FunLike.Basic): beta reduce `CoeFun.coe` (#7905) …
Modified Quaternion.coe_normSq_addView on Github →
2023-05-22 00:38
Mathlib/Algebra/Quaternion.lean
feat: port Algebra.Quaternion (#3776)
Added Quaternion.coe_normSq_addView on Github →