Rename

📁 Source: Mathlib/RingTheory/MvPowerSeries/Rename.lean

Statistics

Metric	Count
Definitions `killCompl`, `killComplFun`, `rename`, `renameEquiv`, `renameFun`	5
Theorems `coeff_embDomain_rename`, `coeff_killCompl`, `coeff_rename`, `coeff_rename_eq_zero`, `constantCoeff_rename`, `killCompl_C`, `killCompl_X`, `killCompl_X_eq_zero`, `killCompl_comp_rename`, `killCompl_map`, `killCompl_monomial_embDomain`, `killCompl_monomial_eq_zero`, `killCompl_rename_app`, `renameEquiv_apply`, `renameEquiv_refl`, `renameEquiv_symm`, `renameEquiv_trans`, `rename_C`, `rename_X`, `rename_coe`, `rename_comp_rename`, `rename_id`, `rename_id_apply`, `rename_inj`, `rename_injective`, `rename_map`, `rename_monomial`, `rename_rename`	28
Total	33

MvPowerSeries

Definitions

Name	Category	Theorems
`killCompl` 📖	CompOp	9 math math: `killCompl_comp_rename`, `killCompl_monomial_embDomain`, `killCompl_rename_app`, `killCompl_map`, `killCompl_X_eq_zero`, `killCompl_monomial_eq_zero`, `coeff_killCompl`, `killCompl_X`, `killCompl_C`
`killComplFun` 📖	CompOp	—
`rename` 📖	CompOp	18 math math: `rename_map`, `killCompl_comp_rename`, `coeff_embDomain_rename`, `rename_rename`, `rename_C`, `rename_monomial`, `rename_id`, `rename_id_apply`, `rename_coe`, `killCompl_rename_app`, `rename_inj`, `rename_comp_rename`, `constantCoeff_rename`, `rename_injective`, `renameEquiv_apply`, `coeff_rename_eq_zero`, `coeff_rename`, `rename_X`
`renameEquiv` 📖	CompOp	4 math math: `renameEquiv_symm`, `renameEquiv_refl`, `renameEquiv_apply`, `renameEquiv_trans`
`renameFun` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_embDomain_rename` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `Finsupp.embDomain` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `Function.Embedding` `Function.instFunLikeEmbedding` `Filter.TendstoCofinite.embedding`	—	`Filter.TendstoCofinite.embedding` `Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite` `coeff_rename` `Finset.sum_eq_single` `instIsEmptyFalse`
`coeff_killCompl` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `Finsupp.embDomain` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	—
`coeff_rename` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `Finset.sum` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Set.Finite.toFinset` `Set.preimage` `Finsupp.mapDomain` `Set` `Set.instSingletonSet` `Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite`	—	—
`coeff_rename_eq_zero` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Set.instMembership` `Set.range` `Finsupp.mapDomain`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite` `coeff_rename` `Finset.sum_congr` `Set.toFinset_congr` `Set.preimage_singleton_eq_empty` `Set.toFinset_empty`
`constantCoeff_rename` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `constantCoeff` `AlgHom` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`coeff_zero_eq_constantCoeff_apply` `Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite` `coeff_rename` `Finset.sum_eq_single` `Unique.instSubsingleton` `instIsEmptyFalse` `Finsupp.mapDomain_zero`
`killCompl_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`killCompl_monomial_embDomain`
`killCompl_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `X` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`ext` `coeff_killCompl` `coeff_X`
`killCompl_X_eq_zero` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `X` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finsupp.mem_range_embDomain_iff` `Finsupp.support_single_ne_zero` `Finset.coe_singleton` `Set.singleton_subset_iff` `killCompl_monomial_eq_zero`
`killCompl_comp_rename` 📖	mathematical	—	`AlgHom.comp` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `killCompl` `rename` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Filter.TendstoCofinite.embedding` `AlgHom.id`	—	`AlgHom.ext` `Filter.TendstoCofinite.embedding` `ext` `coeff_killCompl` `coeff_embDomain_rename`
`killCompl_map` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `map`	—	`ext` `coeff_killCompl`
`killCompl_monomial_embDomain` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `Finsupp.embDomain` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	—
`killCompl_monomial_eq_zero` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set` `Set.instMembership` `Set.range` `Finsupp.embDomain`	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`killCompl_rename_app` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `killCompl` `rename` `Function.Embedding` `Function.instFunLikeEmbedding` `Filter.TendstoCofinite.embedding`	—	`AlgHom.congr_fun` `Filter.TendstoCofinite.embedding` `killCompl_comp_rename`
`renameEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `renameEquiv` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `AlgHom.toRingHom` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Filter.TendstoCofinite.equiv`	—	—
`renameEquiv_refl` 📖	mathematical	—	`renameEquiv` `Equiv.refl` `AlgEquiv.refl` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id`	—	`AlgEquiv.ext` `Filter.TendstoCofinite.equiv` `rename_id`
`renameEquiv_symm` 📖	mathematical	—	`AlgEquiv.symm` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `renameEquiv` `Equiv.symm`	—	—
`renameEquiv_trans` 📖	mathematical	—	`AlgEquiv.trans` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `renameEquiv` `Equiv.trans`	—	`AlgEquiv.ext` `rename_rename` `Filter.TendstoCofinite.equiv`
`rename_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`rename_monomial`
`rename_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `X`	—	`Finsupp.mapDomain_single` `rename_monomial`
`rename_coe` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `MvPolynomial.toMvPowerSeries` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `MvPolynomial.rename`	—	`MvPolynomial.induction_on` `MvPolynomial.coe_C` `rename_C` `MvPolynomial.algHom_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `MvPolynomial.coe_mul` `MvPolynomial.coe_X` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `rename_X` `MvPolynomial.rename_X`
`rename_comp_rename` 📖	mathematical	—	`AlgHom.comp` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `rename` `Filter.TendstoCofinite.comp`	—	`AlgHom.ext` `Filter.TendstoCofinite.comp` `rename_rename`
`rename_id` 📖	mathematical	—	`rename` `Filter.TendstoCofinite.id` `AlgHom.id` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id`	—	`AlgHom.ext` `Filter.TendstoCofinite.id` `ext` `Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite` `coeff_rename` `Finset.sum_eq_single` `Finsupp.mapDomain_id` `instIsEmptyFalse`
`rename_id_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `Filter.TendstoCofinite.id`	—	`Filter.TendstoCofinite.id` `rename_id`
`rename_inj` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `Function.Embedding` `Function.instFunLikeEmbedding` `Filter.TendstoCofinite.embedding`	—	`Filter.TendstoCofinite.embedding` `rename_injective`
`rename_injective` 📖	mathematical	—	`MvPowerSeries` `DFunLike.coe` `AlgHom` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `Function.Embedding` `Function.instFunLikeEmbedding` `Filter.TendstoCofinite.embedding`	—	`Filter.TendstoCofinite.embedding` `ext` `coeff_embDomain_rename` `ext_iff`
`rename_map` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `map`	—	`ext` `Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite` `coeff_rename` `Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`rename_monomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `Finsupp.mapDomain` `Nat.instAddCommMonoid`	—	—
`rename_rename` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `rename` `Filter.TendstoCofinite.comp`	—	`ext` `Filter.TendstoCofinite.comp` `Filter.TendstoCofinite.finite_preimage_singleton` `Finsupp.mapDomain_tendstoCofinite` `coeff_rename` `Finset.sum_congr` `Finset.sum_finset_product'` `Finset.sum_image` `Set.Finite.coe_toFinset`

---

← Back to Index