Commit 2024-08-05 08:52 145e6ba7

View on Github →

chore(CstarAlgebra/Module): drop DecidableEq assumptions (#15489) Also reuse map_sum instead of proving by induction.

Estimated changes

Modified Mathlib/Analysis/CstarAlgebra/Module.lean

modified theorem CstarModule.inner_sum_left

modified theorem CstarModule.inner_sum_right