Ext

📁 Source: Mathlib/Data/Finsupp/Ext.lean

Statistics

Metric	Count
Definitions	0
Theorems addHom_ext, addHom_ext', addHom_ext'_iff, add_closure_setOf_eq_single, mulHom_ext, mulHom_ext', mulHom_ext'_iff	7
Total	7

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHom_ext 📖	—	DFunLike.coe AddMonoidHom Finsupp AddZero.toZero AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike single	—	—	AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single
addHom_ext' 📖	—	AddMonoidHom.comp Finsupp AddZero.toZero AddZeroClass.toAddZero instAddZeroClass singleAddHom	—	—	addHom_ext DFunLike.congr_fun
addHom_ext'_iff 📖	mathematical	—	AddMonoidHom.comp Finsupp AddZero.toZero AddZeroClass.toAddZero instAddZeroClass singleAddHom	—	addHom_ext'
add_closure_setOf_eq_single 📖	mathematical	—	AddSubmonoid.closure Finsupp AddZero.toZero AddZeroClass.toAddZero instAddZeroClass setOf single Top.top AddSubmonoid AddSubmonoid.instTop	—	top_unique induction AddSubmonoid.zero_mem AddSubmonoid.add_mem AddSubmonoid.subset_closure
mulHom_ext 📖	—	DFunLike.coe MonoidHom Multiplicative Finsupp AddZero.toZero AddZeroClass.toAddZero MulOneClass.toMulOne Multiplicative.mulOneClass instAddZeroClass MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd single	—	—	MonoidHom.ext DFunLike.congr_fun addHom_ext Multiplicative.monoidHom_ext addHom_ext' AddMonoidHom.ext Additive.ext DFunLike.ext_iff
mulHom_ext' 📖	—	MonoidHom.comp Multiplicative Finsupp AddZero.toZero AddZeroClass.toAddZero MulOneClass.toMulOne Multiplicative.mulOneClass instAddZeroClass DFunLike.coe Equiv AddMonoidHom MonoidHom EquivLike.toFunLike Equiv.instEquivLike AddMonoidHom.toMultiplicative singleAddHom	—	—	mulHom_ext DFunLike.congr_fun
mulHom_ext'_iff 📖	mathematical	—	MonoidHom.comp Multiplicative Finsupp AddZero.toZero AddZeroClass.toAddZero MulOneClass.toMulOne Multiplicative.mulOneClass instAddZeroClass DFunLike.coe Equiv AddMonoidHom MonoidHom EquivLike.toFunLike Equiv.instEquivLike AddMonoidHom.toMultiplicative singleAddHom	—	mulHom_ext'

---

← Back to Index