Diff — Linear map

Revision #2114 → #2827 · back to history

addedAdditivity axiomc1213247c544

addedHomogeneity axiom40ebcfc07639

addedGeneralization to modules537f947fc343

modifiedRotation by 90 degrees counterclockwise8ebedc52c522

Field	From #2114	To #2827
mathlib.match_kind	special_case	generalization
note	Mathlib has 2D rotation matrices via `Matrix.planeConformalMatrix`, but no dedicated `rotation_by_90` example.	Mathlib has 2D rotation matrices as a special case of `Matrix.planeConformalMatrix` (rotation + scaling), but no dedicated `rotation_by_90` example.
provenance	ai	ai-moderated

addedFredholm operator28346fa85170

addedAtiyah–Singer index theorem4a4c954a6ea6

addedContinuous linear operator848bb3876b7f