bi)jective is local (for linear maps).
#17472

Open

feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps). #17472

erdOne wants to merge 13 commits into master from bijective_local

first commit

68027d6d

first commit

462ad3fc

add stuff

846d4a24

add and move

f9d2a546

erdOne added awaiting-review

erdOne added t-algebra

Update local_properties.lean

7a481e33

Update local_properties.lean

2f3cb777

joelriou commented on 2022-11-17

Update src/ring_theory/local_properties.lean

9376ba1e

Merge branch 'bijective_local' of https://github.com/leanprover-commu…

5425ad39

oops

1c6d66e0

add docs

8ec38b19

add docs

943bf1dc

generalize stuff

25aab4c3

add docs

8aa5aae3

Vierkantor assigned

Vierkantor 2 years ago

Vierkantor commented on 2023-01-03

Vierkantor removed awaiting-review

Vierkantor added awaiting-author

kim-em added too-late

Reviewers

Vierkantor

joelriou

Assignees

Vierkantor

Labels

awaiting-author t-algebra too-late

Milestone

No milestone

mathlib3 feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps). #17472 Open

feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps). #17472

mathlib3
feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps).
#17472

Open