Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 15:00 e1820854

View on Github →

feat(ring_theory/is_tensor_product): Universal property of base change (#15800)

Estimated changes

Modified src/ring_theory/is_tensor_product.lean

added theorem is_base_change.alg_hom_ext'

added theorem is_base_change.alg_hom_ext

added theorem is_base_change.comm

added theorem is_base_change.comp

added theorem is_base_change.iff_lift_unique

added theorem is_base_change.induction_on

added theorem is_base_change.of_equiv

added theorem is_base_change.of_lift_unique

added theorem is_base_change.symm