Commit 2023-05-21 08:32 46527bed

View on Github →

feat: port Analysis.NormedSpace.Star.Mul (#4147)

Estimated changes

added theorem mul_flip_isometry
added theorem mul_isometry
added theorem op_nnnorm_mul
added theorem op_nnnorm_mul_flip