Commit 2024-11-18 15:35 f2ac82b1

View on Github →

chore(FieldTheory/PurelyInseparable): fix typo _of_isIntegral' -> _of_isSeparable' (#19182)

Estimated changes

Modified Mathlib/FieldTheory/PurelyInseparable.lean

deleted theorem LinearIndependent.map_pow_expChar_pow_of_isIntegral'

added theorem LinearIndependent.map_pow_expChar_pow_of_isSeparable'