Commit 2022-07-02 10:12 2d76f563

View on Github →

chore(algebra/associated): make irreducible not a class (#14713) This functionality was rarely used and doesn't align with how irreducible is used in practice. In a future PR, we can remove some unfreezingIs caused by this.

Estimated changes

Modified src/algebra/associated.lean

deleted theorem irreducible.not_unit

added structure irreducible

Modified src/algebra/module/pid.lean

Modified src/field_theory/adjoin.lean

Modified src/field_theory/normal.lean

Modified src/field_theory/separable_degree.lean

added theorem irreducible.has_separable_contraction

deleted theorem polynomial.irreducible_has_separable_contraction

Modified src/field_theory/splitting_field.lean

added theorem polynomial.fact_irreducible_factor

added theorem polynomial.irreducible_factor

Modified src/number_theory/number_field.lean

Modified src/ring_theory/adjoin_root.lean

added theorem adjoin_root.coe_injective'

modified theorem adjoin_root.coe_injective

modified theorem adjoin_root.mul_div_root_cancel