FormalConjecturesForMathlib/Algebra/Polynomial/HasseDeriv.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. theorem Polynomial.hasseDeriv_map line 24 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Semiring, RingHom, Nat, Polynomial, Eq, LinearMap, RingHom.id, Polynomial.hasseDeriv, Polynomial.map

    Proof uses: Polynomial.ext, of_eq_true, Polynomial.coeff, Eq.trans, HMul.hMul, Nat.choose, HAdd.hAdd, True, congr, congrArg, Polynomial.hasseDeriv_coeff, Polynomial.coeff_map, map_mul, congrFun', map_natCast, eq_self

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.