Skip to content
This repository was 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
tb65536 wants to merge 1 commit into
masterfrom
tb_rename
Open

refactor(linear_algebra/*): Rename linear_equiv.range to linear_equiv.range_eq_top#18969
tb65536 wants to merge 1 commit into
masterfrom
tb_rename

Conversation

@tb65536

@tb65536 tb65536 commented May 8, 2023

Copy link
Copy Markdown
Collaborator

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