Theorem ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit

Modification history