OfFn

📁 Source: Mathlib/Algebra/Polynomial/OfFn.lean

Statistics

Metric	Count
Definitions ofFn, toFn	2
Theorems injective_ofFn, ne_zero_of_ofFn_ne_zero, ofFn_coeff_eq_val_of_lt, ofFn_coeff_eq_zero_of_ge, ofFn_comp_toFn_eq_id_of_natDegree_lt, ofFn_degree_lt, ofFn_eq_sum_monomial, ofFn_natDegree_lt, ofFn_zero, ofFn_zero', surjective_toFn, toFn_comp_ofFn_eq_id, toFn_zero	13
Total	15

Polynomial

Definitions

Name	Category	Theorems
ofFn 📖	CompOp	10 math math: ofFn_zero, ofFn_eq_sum_monomial, ofFn_zero', toFn_comp_ofFn_eq_id, injective_ofFn, ofFn_degree_lt, ofFn_comp_toFn_eq_id_of_natDegree_lt, ofFn_coeff_eq_val_of_lt, ofFn_coeff_eq_zero_of_ge, ofFn_natDegree_lt
toFn 📖	CompOp	4 math math: toFn_zero, toFn_comp_ofFn_eq_id, surjective_toFn, ofFn_comp_toFn_eq_id_of_natDegree_lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_ofFn 📖	mathematical	—	Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn	—	toFn_comp_ofFn_eq_id
ne_zero_of_ofFn_ne_zero 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose₄
ofFn_coeff_eq_val_of_lt 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn	—	coeff_ofFinsupp
ofFn_coeff_eq_zero_of_ge 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	coeff_ofFinsupp
ofFn_comp_toFn_eq_id_of_natDegree_lt 📖	mathematical	natDegree	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn toFn	—	ext ofFn_coeff_eq_val_of_lt coeff_eq_zero_of_natDegree_lt ofFn_coeff_eq_zero_of_ge
ofFn_degree_lt 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	—	natDegree_lt_iff_degree_lt ofFn_natDegree_lt ne_zero_of_ofFn_ne_zero
ofFn_eq_sum_monomial 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn Finset.sum Finset.univ Fin.fintype monomial	—	List.toFinsupp.congr_simp List.toFinsupp_nil Finset.sum_congr Finset.univ_eq_empty Fin.isEmpty' as_sum_range' ofFn_natDegree_lt Finset.sum_range ofFn_coeff_eq_val_of_lt
ofFn_natDegree_lt 📖	mathematical	—	natDegree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn	—	natDegree_le_iff_coeff_eq_zero ofFn_coeff_eq_zero_of_ge
ofFn_zero 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instZero	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
ofFn_zero' 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.Function.module Semiring.toModule module LinearMap.instFunLike ofFn instZero	—	—
surjective_toFn 📖	mathematical	—	Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.addCommMonoid module Semiring.toModule Pi.Function.module LinearMap.instFunLike toFn	—	toFn_comp_ofFn_eq_id
toFn_comp_ofFn_eq_id 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.addCommMonoid module Semiring.toModule Pi.Function.module LinearMap.instFunLike toFn ofFn	—	coeff_ofFinsupp
toFn_zero 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Pi.addCommMonoid module Semiring.toModule Pi.Function.module LinearMap.instFunLike toFn instZero Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass

---

← Back to Index