Commit 2024-07-19 14:02 869e6bb7

View on Github →

feat (LinearAlgebra/FreeProduct): introduce basic structure, universal property (#14858) Adds the free product of algebras, together with its universal property, in preparation for invoking it in a future Category.AlgebraCat.FilteredColimits.lean.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FreeProduct/Basic.lean

added theorem DirectSum.induction_lon

added theorem LinearAlgebra.FreeProduct.identify_one

added def LinearAlgebra.FreeProduct.lift

added theorem LinearAlgebra.FreeProduct.lift_comp_ι

added theorem LinearAlgebra.FreeProduct.lift_unique

added theorem LinearAlgebra.FreeProduct.lof_map_one

added theorem LinearAlgebra.FreeProduct.mul_injections

added def LinearAlgebra.FreeProduct.rel'

added inductive LinearAlgebra.FreeProduct.rel

added theorem LinearAlgebra.FreeProduct.rel_id

added theorem LinearAlgebra.FreeProduct.ι_apply

added def LinearAlgebra.FreeProduct

added def LinearAlgebra.FreeProduct_ofPowers

added def RingQuot.algEquiv_quot_algEquiv

added def RingQuot.equiv_quot_equiv