Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-16 13:27 565eb991

View on Github →

chore(*): remove after the fact attribute [irreducible] at several places (#18168) Part of #18164

Estimated changes

modified def free_algebra.lift
modified theorem free_algebra.lift_aux_eq
modified theorem free_algebra.quot_mk_eq_ι
modified def free_algebra.ι
modified def ring_quot.lift
modified def ring_quot.mk_alg_hom
modified def ring_quot.mk_ring_hom
modified theorem polynomial.comp_eq_sum_left
modified def polynomial.eval₂
modified theorem polynomial.eval₂_eq_sum
modified def linear_map.det_aux
modified def span.repr
modified def tensor_algebra.ι
modified theorem fractional_ideal.coe_mul