Ext

Statistics

Metric	Count
Definitions	0
Theorems `addHom_ext`, `addHom_ext'`, `addHom_ext'_iff`, `add_closure_iUnion_range_single`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`addHom_ext` 📖	—	`DFunLike.coe` `AddMonoidHom` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom.instFunLike` `single`	—	—	`AddMonoidHom.eq_of_eqOn_denseM` `add_closure_iUnion_range_single`
`addHom_ext'` 📖	—	`AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `singleAddHom`	—	—	`addHom_ext` `DFunLike.congr_fun`
`addHom_ext'_iff` 📖	mathematical	—	`AddMonoidHom.comp` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `singleAddHom`	—	`addHom_ext'`
`add_closure_iUnion_range_single` 📖	mathematical	—	`AddSubmonoid.closure` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `addZeroClass` `Set.iUnion` `Set.range` `single` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop`	—	`top_unique` `induction` `AddSubmonoid.zero_mem` `AddSubmonoid.add_mem` `AddSubmonoid.subset_closure` `Set.mem_iUnion` `Set.mem_range_self`

---