mathlib3
b5e832e2 - refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp` (#5796)

Commit

5 years ago

refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp` (#5796) faster proofs and smaller proof terms Co-authors: `lean-gptf`, Yuhuai Wu

Author

Jesse Michael Han

Parents

57bc1dab

mathlib3 b5e832e2 - refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp` (#5796)

mathlib3
b5e832e2 - refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp` (#5796)