Commit 2025-02-07 08:12 bbbf03a5

View on Github →

chore(Analysis/NormedSpace/OperatorNorm/Mul): don't use 𝕜' for a ring (#21506) I am finding it particularly confusing to use 𝕜something for a ring when 𝕜 is already used for a type playing a completely different role. From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

modified theorem ContinuousLinearMap.coe_mulₗᵢ

modified theorem ContinuousLinearMap.isometry_mul

modified def ContinuousLinearMap.lsmul

modified theorem ContinuousLinearMap.lsmul_apply

modified def ContinuousLinearMap.mul

modified def ContinuousLinearMap.mulLeftRight

modified theorem ContinuousLinearMap.mulLeftRight_apply

modified theorem ContinuousLinearMap.mul_apply'

modified def ContinuousLinearMap.mulₗᵢ

modified theorem ContinuousLinearMap.opNNNorm_mul

modified theorem ContinuousLinearMap.opNNNorm_mul_apply

modified theorem ContinuousLinearMap.opNorm_lsmul

modified theorem ContinuousLinearMap.opNorm_lsmul_apply_le

modified theorem ContinuousLinearMap.opNorm_lsmul_le

modified theorem ContinuousLinearMap.opNorm_mul

modified theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le

modified theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le

modified theorem ContinuousLinearMap.opNorm_mul_apply

modified theorem ContinuousLinearMap.opNorm_mul_apply_le

modified theorem ContinuousLinearMap.opNorm_mul_le

modified def NonUnitalAlgHom.Lmul

modified theorem NonUnitalAlgHom.coe_Lmul