Commit 2025-10-21 12:12 df398e56

View on Github →

feat(FieldTheory/RatFunc/Basic): add characteristic instances for RatFunc (#29356)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem algebraMap.coe_eq_zero_iff

added theorem algebraMap.coe_inj

added theorem algebraMap.lift_map_eq_zero_iff

Modified Mathlib/Algebra/Algebra/Field.lean

deleted theorem algebraMap.coe_inj

deleted theorem algebraMap.lift_map_eq_zero_iff

Created Mathlib/Algebra/Algebra/IsSimpleRing.lean

Modified Mathlib/Algebra/CharP/Algebra.lean

added theorem ExpChar.of_injective_algebraMap'

modified theorem charP_of_injective_algebraMap'

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/FieldTheory/Differential/Liouville.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean