is_tensor_product): Base change along a surjection.
#17010

Open

feat(src/ring_theory/is_tensor_product): Base change along a surjection. #17010

erdOne wants to merge 2 commits into master from is_tensor_product_of_surjective

first commit

c2a59f2b

erdOne added awaiting-review

erdOne added t-algebra

Update is_tensor_product.lean

03399e9f

github-actions added ready-to-merge

github-actions removed awaiting-review

github-actions added delegated

kim-em removed ready-to-merge

kim-em removed delegated

kim-em added awaiting-review

kim-em added not-too-late

erdOne closed this 2 years ago

erdOne removed not-too-late

erdOne added too-late

erdOne reopened this 2 years ago

github-actions added modifies-synchronized-file

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review t-algebra modifies-synchronized-file too-late

Milestone

No milestone