Theorem ExpChar.of_injective_algebraMap'

Modification history

2025-10-21 12:12

Mathlib/Algebra/CharP/Algebra.lean

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

Added ExpChar.of_injective_algebraMap'View on Github →