Commit 2026-09-08 10:36 bc7422b4
View on Github →chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass (#43376)
This rename is a small part of #31365, step (2) and the analogue of #43368 for semi-linear maps.
In addition, this PR goes one step further by removing the existing LinearMap.ofClass: both definitions mean the same, so we only need one. Note that neither LinearMap nor SemilinearMap is a definition, and LinearMapClass is defined in terms of SemilinearMapClass.
Rename a few lemmas using ofClass, so their names match the naming convention.
And delete LinearMap.coe_semilinearMap, which would have been misnamed now, as an exact duplicate of the now-called LinearMap.coe_ofClass.