Commit 2023-05-25 12:49 83cb97a0

View on Github →

feat: port RingTheory.IsTensorProduct (#4227)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/IsTensorProduct.lean

added theorem Algebra.IsPushout.algHom_ext

added theorem Algebra.IsPushout.comm

added theorem Algebra.IsPushout.symm

added theorem Algebra.lift_algHom_comp_left

added theorem Algebra.lift_algHom_comp_right

added theorem Algebra.pushoutDesc_apply

added theorem Algebra.pushoutDesc_left

added theorem Algebra.pushoutDesc_right

added theorem IsBaseChange.alg_hom_ext'

added theorem IsBaseChange.alg_hom_ext

added theorem IsBaseChange.comp

added theorem IsBaseChange.equiv_symm_apply

added theorem IsBaseChange.equiv_tmul

added theorem IsBaseChange.iff_lift_unique

added theorem IsBaseChange.lift_comp

added theorem IsBaseChange.ofEquiv

added theorem IsBaseChange.of_lift_unique

added def IsBaseChange

added theorem IsTensorProduct.equiv_symm_apply

added theorem IsTensorProduct.equiv_toLinearMap

added theorem IsTensorProduct.inductionOn

added theorem IsTensorProduct.lift_eq

added theorem IsTensorProduct.map_eq

added def IsTensorProduct

added theorem TensorProduct.isBaseChange

added theorem TensorProduct.isTensorProduct