Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

refactor(linear_algebra/*): Rename linear_equiv.range to linear_equiv.range_eq_top #18969

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented May 8, 2023

This rename was suggested by @eric-wieser on #18959


Open in Gitpod

@tb65536 tb65536 added WIP Work in progress awaiting-CI The author would like to see what CI has to say before doing more work. labels May 8, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 8, 2023
@tb65536 tb65536 changed the title refactor(linear_algebra/*): Rename alg_equiv.range to alg_equiv.range_eq_top refactor(linear_algebra/*): Rename linear_equiv.range to linear_equiv.range_eq_top May 12, 2023
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
awaiting-CI The author would like to see what CI has to say before doing more work. modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. too-late This PR was ready too late for inclusion in mathlib3 WIP Work in progress
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants