Funext

Statistics

Metric	Count
Definitions	0
Theorems `funext`, `funext_iff`, `funext_set`, `funext_set_iff`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`funext` 📖	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `eval`	—	—	`funext_set` `Set.infinite_univ`
`funext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `eval`	—	`Nontrivial.to_nonempty` `IsDomain.toNontrivial` `funext`
`funext_set` 📖	—	`Set.Infinite` `DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `eval`	—	—	`exists_fin_rename` `eval₂Hom_rename` `Function.extend_comp` `em` `Function.Injective.extend_apply` `Set.Infinite.nonempty` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_self`
`funext_set_iff` 📖	mathematical	`Set.Infinite`	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `eval`	—	`funext_set`

---