Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-12 05:40 825b341b

View on Github →

feat(ring_theory/is_tensor_product): Add predicate algebra.is_pushout. (#17197)

Estimated changes

Modified src/ring_theory/is_tensor_product.lean

added theorem algebra.is_pushout.alg_hom_ext

added theorem algebra.is_pushout.comm

added theorem algebra.is_pushout.symm

added theorem algebra.lift_alg_hom_comp_left

added theorem algebra.lift_alg_hom_comp_right

added def algebra.pushout_desc

added theorem algebra.pushout_desc_left

added theorem algebra.pushout_desc_right

deleted theorem is_base_change.comm

deleted theorem is_base_change.symm