Commit 2024-11-14 06:25 68537a00

View on Github →

refactor(RingHom.injective): use simple ring (#18868)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Field.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/Field/Basic.lean

Modified Mathlib/Algebra/Field/Subfield/Basic.lean

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/Data/ENat/Lattice.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Deprecated/Subfield.lean

Modified Mathlib/FieldTheory/Galois/GaloisClosure.lean

Modified Mathlib/FieldTheory/NormalClosure.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/SimpleRing/Basic.lean

deleted theorem IsSimpleRing.injective_ringHom

deleted theorem IsSimpleRing.isField_center

deleted theorem isSimpleRing_iff_isField

Created Mathlib/RingTheory/SimpleRing/Field.lean

added theorem IsSimpleRing.isField_center

added theorem isSimpleRing_iff_isField

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

deleted theorem TwoSidedIdeal.coe_mop_smul

deleted theorem TwoSidedIdeal.coe_smul

deleted def TwoSidedIdeal.subtype

deleted def TwoSidedIdeal.subtypeMop

Created Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean

added def TwoSidedIdeal.ker

added theorem TwoSidedIdeal.ker_eq_bot

added theorem TwoSidedIdeal.ker_ringCon

added theorem TwoSidedIdeal.ker_ringCon_mk'

added theorem TwoSidedIdeal.mem_ker

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

added theorem TwoSidedIdeal.coe_mop_smul

added theorem TwoSidedIdeal.coe_smul

deleted def TwoSidedIdeal.ker

deleted theorem TwoSidedIdeal.ker_eq_bot

deleted theorem TwoSidedIdeal.ker_ringCon_mk'

deleted theorem TwoSidedIdeal.mem_ker

added def TwoSidedIdeal.subtype

added def TwoSidedIdeal.subtypeMop

Modified Mathlib/RingTheory/Valuation/ValExtension.lean

Modified scripts/noshake.json