Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-11 08:22 f30200e5

View on Github →

refactor(algebra/free_algebra): Make lift an equiv (#4908) This can probably lead to some API cleanup down the line

Estimated changes

Modified src/algebra/category/Algebra/basic.lean

Modified src/algebra/free_algebra.lean

modified def free_algebra.lift

added theorem free_algebra.lift_aux_eq

added theorem free_algebra.lift_symm_apply

Modified src/algebra/lie/universal_enveloping.lean

modified def universal_enveloping_algebra.lift

added theorem universal_enveloping_algebra.lift_symm_apply

modified theorem universal_enveloping_algebra.ι_comp_lift

Modified src/algebra/ring_quot.lean

modified def ring_quot.lift

modified def ring_quot.lift_alg_hom

Modified src/linear_algebra/clifford_algebra.lean

modified def clifford_algebra.lift

Modified src/linear_algebra/exterior_algebra.lean

modified theorem exterior_algebra.hom_ext

modified def exterior_algebra.lift

Modified src/linear_algebra/tensor_algebra.lean

modified def tensor_algebra.lift