Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:50 038e0b27

View on Github →

feat(ring_theory/algebra): remove out_param

Estimated changes

modified def alg_hom.comap
modified theorem alg_hom.commutes
modified def alg_hom.comp
modified theorem alg_hom.comp_apply
modified theorem alg_hom.comp_assoc
modified theorem alg_hom.comp_id
modified theorem alg_hom.ext
modified theorem alg_hom.id_apply
modified theorem alg_hom.id_comp
modified theorem alg_hom.to_linear_map_inj
modified theorem algebra.lmul_apply
modified theorem algebra.lmul_left_apply
modified theorem algebra.lmul_right_apply
modified theorem algebra.map_add
modified theorem algebra.map_mul
modified theorem algebra.map_neg
modified theorem algebra.map_one
modified theorem algebra.map_sub
modified theorem algebra.map_zero
modified theorem algebra.mem_bot
modified theorem algebra.of_id_apply
deleted def algebra.of_subring
modified def algebra.to_comap
modified theorem algebra.to_comap_apply
modified def algebra.to_top
modified def algebra_map
modified def mv_polynomial.aeval
modified theorem mv_polynomial.eval_unique
modified def polynomial.aeval
modified theorem polynomial.eval_unique
modified def subalgebra.val