Algebra

📁 Source: Mathlib/Topology/LocallyConstant/Algebra.lean

Statistics

Metric	Count
Definitions `charFn`, `coeFnAddMonoidHom`, `coeFnAlgHom`, `coeFnMonoidHom`, `coeFnRingHom`, `coeFnₗ`, `comapAddMonoidHom`, `comapMonoidHom`, `comapRingHom`, `comapₐ`, `comapₗ`, `congrLeftRingEquiv`, `congrLeftₐ`, `congrLeftₗ`, `congrRightRingEquiv`, `congrRightₐ`, `congrRightₗ`, `constAddMonoidHom`, `constMonoidHom`, `constRingHom`, `constₐ`, `constₗ`, `evalAddMonoidHom`, `evalMonoidHom`, `evalRingHom`, `evalₐ`, `evalₗ`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddCommSemigroup`, `instAddGroup`, `instAddMonoid`, `instAddMonoidWithOne`, `instAddSemigroup`, `instAddZeroClass`, `instAlgebra`, `instCommGroup`, `instCommMonoid`, `instCommRing`, `instCommSemigroup`, `instCommSemiring`, `instDistrib`, `instDistribMulAction`, `instDiv`, `instGroup`, `instIntCast`, `instInv`, `instModule`, `instMonoid`, `instMul`, `instMulAction`, `instMulOneClass`, `instMulZeroClass`, `instMulZeroOneClass`, `instNatCast`, `instNeg`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instOne`, `instPow`, `instRing`, `instSemigroup`, `instSemigroupWithZero`, `instSemiring`, `instSub`, `instZero`, `mapAddMonoidHom`, `mapMonoidHom`, `mapRingHom`, `mapₐ`, `mapₗ`, `smul`, `vadd`	80
Theorems `add_apply`, `charFn_eq_one`, `charFn_eq_zero`, `charFn_inj`, `coeFnAddMonoidHom_apply`, `coeFnAlgHom_apply`, `coeFnMonoidHom_apply`, `coeFnRingHom_apply`, `coeFnₗ_apply`, `coe_add`, `coe_algebraMap`, `coe_charFn`, `coe_div`, `coe_inv`, `coe_mul`, `coe_neg`, `coe_one`, `coe_smul`, `coe_sub`, `coe_vadd`, `coe_zero`, `comapAddMonoidHom_apply`, `comapMonoidHom_apply`, `comapRingHom_apply_apply`, `comapₐ_apply_apply`, `comapₗ_apply_apply`, `congrLeftRingEquiv_apply_apply`, `congrLeftRingEquiv_symm_apply_apply`, `congrLeftₐ_apply_apply`, `congrLeftₐ_symm_apply_apply`, `congrLeftₗ_apply_apply`, `congrLeftₗ_symm_apply_apply`, `congrRightRingEquiv_apply_apply`, `congrRightRingEquiv_symm_apply_apply`, `congrRightₐ_apply_apply`, `congrRightₐ_symm_apply_apply`, `congrRightₗ_apply_apply`, `congrRightₗ_symm_apply_apply`, `constAddMonoidHom_apply`, `constMonoidHom_apply`, `constRingHom_apply`, `constₐ_apply_apply`, `constₗ_apply_apply`, `div_apply`, `evalAddMonoidHom_apply`, `evalMonoidHom_apply`, `evalRingHom_apply`, `evalₐ_apply`, `evalₗ_apply`, `inv_apply`, `ker_comapₗ`, `mapAddMonoidHom_apply`, `mapMonoidHom_apply`, `mapRingHom_apply_apply`, `mapₐ_apply_apply`, `mapₗ_apply_apply`, `mul_apply`, `neg_apply`, `one_apply`, `smul_apply`, `sub_apply`, `vadd_apply`, `zero_apply`	63
Total	143

LocallyConstant

Definitions

Name	Category	Theorems
`charFn` 📖	CompOp	3 math math: `charFn_eq_one`, `charFn_eq_zero`, `coe_charFn`
`coeFnAddMonoidHom` 📖	CompOp	1 math math: `coeFnAddMonoidHom_apply`
`coeFnAlgHom` 📖	CompOp	1 math math: `coeFnAlgHom_apply`
`coeFnMonoidHom` 📖	CompOp	1 math math: `coeFnMonoidHom_apply`
`coeFnRingHom` 📖	CompOp	1 math math: `coeFnRingHom_apply`
`coeFnₗ` 📖	CompOp	1 math math: `coeFnₗ_apply`
`comapAddMonoidHom` 📖	CompOp	1 math math: `comapAddMonoidHom_apply`
`comapMonoidHom` 📖	CompOp	1 math math: `comapMonoidHom_apply`
`comapRingHom` 📖	CompOp	1 math math: `comapRingHom_apply_apply`
`comapₐ` 📖	CompOp	1 math math: `comapₐ_apply_apply`
`comapₗ` 📖	CompOp	4 math math: `CompHausLike.LocallyConstantModule.functorToPresheaves_map_app`, `comapₗ_apply_apply`, `CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map`, `ker_comapₗ`
`congrLeftRingEquiv` 📖	CompOp	2 math math: `congrLeftRingEquiv_apply_apply`, `congrLeftRingEquiv_symm_apply_apply`
`congrLeftₐ` 📖	CompOp	2 math math: `congrLeftₐ_apply_apply`, `congrLeftₐ_symm_apply_apply`
`congrLeftₗ` 📖	CompOp	2 math math: `congrLeftₗ_symm_apply_apply`, `congrLeftₗ_apply_apply`
`congrRightRingEquiv` 📖	CompOp	2 math math: `congrRightRingEquiv_apply_apply`, `congrRightRingEquiv_symm_apply_apply`
`congrRightₐ` 📖	CompOp	2 math math: `congrRightₐ_apply_apply`, `congrRightₐ_symm_apply_apply`
`congrRightₗ` 📖	CompOp	2 math math: `congrRightₗ_symm_apply_apply`, `congrRightₗ_apply_apply`
`constAddMonoidHom` 📖	CompOp	1 math math: `constAddMonoidHom_apply`
`constMonoidHom` 📖	CompOp	1 math math: `constMonoidHom_apply`
`constRingHom` 📖	CompOp	1 math math: `constRingHom_apply`
`constₐ` 📖	CompOp	1 math math: `constₐ_apply_apply`
`constₗ` 📖	CompOp	1 math math: `constₗ_apply_apply`
`evalAddMonoidHom` 📖	CompOp	1 math math: `evalAddMonoidHom_apply`
`evalMonoidHom` 📖	CompOp	2 math math: `evalMonoidHom_apply`, `Profinite.NobelingProof.list_prod_apply`
`evalRingHom` 📖	CompOp	1 math math: `evalRingHom_apply`
`evalₐ` 📖	CompOp	1 math math: `evalₐ_apply`
`evalₗ` 📖	CompOp	1 math math: `evalₗ_apply`
`instAdd` 📖	CompOp	6 math math: `congrLeftRingEquiv_apply_apply`, `add_apply`, `congrLeftRingEquiv_symm_apply_apply`, `congrRightRingEquiv_apply_apply`, `congrRightRingEquiv_symm_apply_apply`, `coe_add`
`instAddCommGroup` 📖	CompOp	37 math math: `Profinite.NobelingProof.injective_πs'`, `Profinite.NobelingProof.Products.span_nil_eq_top`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller`, `Profinite.NobelingProof.coe_πs`, `Profinite.NobelingProof.Products.max_eq_eval`, `Profinite.NobelingProof.Products.eval_πs`, `freeOfProfinite`, `Profinite.NobelingProof.Products.eval_πs'`, `Profinite.NobelingProof.GoodProducts.spanFin`, `Profinite.NobelingProof.succ_exact`, `CompHausLike.LocallyConstantModule.functorToPresheaves_map_app`, `Profinite.NobelingProof.GoodProducts.smaller_factorization`, `Profinite.NobelingProof.πs'_apply_apply`, `Profinite.NobelingProof.Products.eval_πs_image'`, `Profinite.NobelingProof.GoodProducts.span`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller`, `CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum`, `Profinite.NobelingProof.πs_apply_apply`, `Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval`, `Profinite.NobelingProof.GoodProducts.linearIndependent`, `Profinite.NobelingProof.GoodProducts.square_commutes`, `Profinite.NobelingProof.Nobeling_aux`, `Profinite.NobelingProof.spanFinBasis.span`, `Profinite.NobelingProof.GoodProducts.linearIndependentEmpty`, `Profinite.NobelingProof.GoodProducts.span_iff_products`, `Profinite.NobelingProof.CC_comp_zero`, `Profinite.NobelingProof.eval_eq_πJ`, `Profinite.NobelingProof.injective_πs`, `Profinite.NobelingProof.coe_πs'`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range`, `Profinite.NobelingProof.GoodProducts.max_eq_eval`, `Profinite.NobelingProof.GoodProducts.linearIndependentSingleton`, `Profinite.NobelingProof.Products.eval_πs_image`, `CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isAddCommGroup`, `Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply`, `Profinite.NobelingProof.succ_mono`
`instAddCommMonoid` 📖	CompOp	42 math math: `Profinite.NobelingProof.injective_πs'`, `Profinite.NobelingProof.Products.span_nil_eq_top`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller`, `Profinite.NobelingProof.coe_πs`, `congrRightₗ_symm_apply_apply`, `toContinuousMapLinearMap_apply`, `Profinite.NobelingProof.Products.max_eq_eval`, `Profinite.NobelingProof.Products.eval_πs`, `freeOfProfinite`, `Profinite.NobelingProof.Products.eval_πs'`, `Profinite.NobelingProof.GoodProducts.spanFin`, `Profinite.NobelingProof.GoodProducts.smaller_factorization`, `Profinite.NobelingProof.πs'_apply_apply`, `congrRightₗ_apply_apply`, `evalₗ_apply`, `Profinite.NobelingProof.Products.eval_πs_image'`, `Profinite.NobelingProof.GoodProducts.span`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller`, `comapₗ_apply_apply`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum`, `Profinite.NobelingProof.πs_apply_apply`, `Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval`, `Profinite.NobelingProof.GoodProducts.linearIndependent`, `Profinite.NobelingProof.Nobeling_aux`, `Profinite.NobelingProof.spanFinBasis.span`, `congrLeftₗ_symm_apply_apply`, `ker_comapₗ`, `mapₗ_apply_apply`, `congrLeftₗ_apply_apply`, `Profinite.NobelingProof.GoodProducts.linearIndependentEmpty`, `Profinite.NobelingProof.GoodProducts.span_iff_products`, `constₗ_apply_apply`, `Profinite.NobelingProof.CC_comp_zero`, `Profinite.NobelingProof.eval_eq_πJ`, `coeFnₗ_apply`, `Profinite.NobelingProof.injective_πs`, `Profinite.NobelingProof.coe_πs'`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range`, `Profinite.NobelingProof.GoodProducts.max_eq_eval`, `Profinite.NobelingProof.GoodProducts.linearIndependentSingleton`, `Profinite.NobelingProof.Products.eval_πs_image`, `Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply`
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	1 math math: `Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval`
`instAddMonoid` 📖	CompOp	1 math math: `Profinite.NobelingProof.instIsAddTorsionFreeLocallyConstantInt`
`instAddMonoidWithOne` 📖	CompOp	—
`instAddSemigroup` 📖	CompOp	—
`instAddZeroClass` 📖	CompOp	6 math math: `coeFnAddMonoidHom_apply`, `constAddMonoidHom_apply`, `comapAddMonoidHom_apply`, `toContinuousMapAddMonoidHom_apply`, `evalAddMonoidHom_apply`, `mapAddMonoidHom_apply`
`instAlgebra` 📖	CompOp	11 math math: `congrRightₐ_apply_apply`, `congrRightₐ_symm_apply_apply`, `congrLeftₐ_apply_apply`, `mapₐ_apply_apply`, `constₐ_apply_apply`, `coeFnAlgHom_apply`, `congrLeftₐ_symm_apply_apply`, `evalₐ_apply`, `coe_algebraMap`, `toContinuousMapAlgHom_apply`, `comapₐ_apply_apply`
`instCommGroup` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instCommSemigroup` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instDistrib` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instDiv` 📖	CompOp	2 math math: `div_apply`, `coe_div`
`instGroup` 📖	CompOp	—
`instIntCast` 📖	CompOp	—
`instInv` 📖	CompOp	2 math math: `coe_inv`, `inv_apply`
`instModule` 📖	CompOp	14 math math: `CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isModule`, `congrRightₗ_symm_apply_apply`, `toContinuousMapLinearMap_apply`, `CompHausLike.LocallyConstantModule.functorToPresheaves_map_app`, `congrRightₗ_apply_apply`, `evalₗ_apply`, `comapₗ_apply_apply`, `CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map`, `congrLeftₗ_symm_apply_apply`, `ker_comapₗ`, `mapₗ_apply_apply`, `congrLeftₗ_apply_apply`, `constₗ_apply_apply`, `coeFnₗ_apply`
`instMonoid` 📖	CompOp	—
`instMul` 📖	CompOp	12 math math: `congrLeftRingEquiv_apply_apply`, `Profinite.NobelingProof.factors_prod_eq_basis_of_ne`, `coe_mul`, `congrLeftRingEquiv_symm_apply_apply`, `Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval`, `congrRightRingEquiv_apply_apply`, `congrRightRingEquiv_symm_apply_apply`, `mul_apply`, `Profinite.NobelingProof.Products.evalCons`, `Profinite.NobelingProof.list_prod_apply`, `Profinite.NobelingProof.factors_prod_eq_basis`, `Profinite.NobelingProof.factors_prod_eq_basis_of_eq`
`instMulAction` 📖	CompOp	—
`instMulOneClass` 📖	CompOp	7 math math: `comapMonoidHom_apply`, `evalMonoidHom_apply`, `coeFnMonoidHom_apply`, `toContinuousMapMonoidHom_apply`, `mapMonoidHom_apply`, `constMonoidHom_apply`, `Profinite.NobelingProof.list_prod_apply`
`instMulZeroClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instNatCast` 📖	CompOp	—
`instNeg` 📖	CompOp	2 math math: `coe_neg`, `neg_apply`
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	5 math math: `comapRingHom_apply_apply`, `evalRingHom_apply`, `mapRingHom_apply_apply`, `constRingHom_apply`, `coeFnRingHom_apply`
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instOne` 📖	CompOp	7 math math: `one_apply`, `Profinite.NobelingProof.factors_prod_eq_basis_of_ne`, `coe_one`, `Profinite.NobelingProof.one_sub_e_mem_of_false`, `Profinite.NobelingProof.list_prod_apply`, `Profinite.NobelingProof.factors_prod_eq_basis`, `Profinite.NobelingProof.factors_prod_eq_basis_of_eq`
`instPow` 📖	CompOp	—
`instRing` 📖	CompOp	—
`instSemigroup` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—
`instSemiring` 📖	CompOp	11 math math: `congrRightₐ_apply_apply`, `congrRightₐ_symm_apply_apply`, `congrLeftₐ_apply_apply`, `mapₐ_apply_apply`, `constₐ_apply_apply`, `coeFnAlgHom_apply`, `congrLeftₐ_symm_apply_apply`, `evalₐ_apply`, `coe_algebraMap`, `toContinuousMapAlgHom_apply`, `comapₐ_apply_apply`
`instSub` 📖	CompOp	3 math math: `coe_sub`, `sub_apply`, `Profinite.NobelingProof.one_sub_e_mem_of_false`
`instZero` 📖	CompOp	3 math math: `zero_apply`, `coe_zero`, `Profinite.NobelingProof.CC_comp_zero`
`mapAddMonoidHom` 📖	CompOp	1 math math: `mapAddMonoidHom_apply`
`mapMonoidHom` 📖	CompOp	1 math math: `mapMonoidHom_apply`
`mapRingHom` 📖	CompOp	1 math math: `mapRingHom_apply_apply`
`mapₐ` 📖	CompOp	1 math math: `mapₐ_apply_apply`
`mapₗ` 📖	CompOp	2 math math: `CompHausLike.LocallyConstantModule.functorToPresheaves_map_app`, `mapₗ_apply_apply`
`smul` 📖	CompOp	2 math math: `coe_smul`, `smul_apply`
`vadd` 📖	CompOp	2 math math: `vadd_apply`, `coe_vadd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instAdd`	—	—
`charFn_eq_one` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `charFn` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Set` `Set.instMembership`	—	`Set.indicator_eq_one_iff_mem`
`charFn_eq_zero` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `charFn` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `Set` `Set.instMembership`	—	`Set.indicator_eq_zero_iff_notMem`
`charFn_inj` 📖	—	`IsClopen` `charFn`	—	—	—
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `LocallyConstant` `AddZeroClass.toAddZero` `instAddZeroClass` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLike`	—	—
`coeFnAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `LocallyConstant` `instSemiring` `Pi.semiring` `instAlgebra` `Function.algebra` `AlgHom.funLike` `coeFnAlgHom` `instFunLike`	—	—
`coeFnMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LocallyConstant` `MulOneClass.toMulOne` `instMulOneClass` `Pi.mulOneClass` `MonoidHom.instFunLike` `coeFnMonoidHom` `instFunLike`	—	—
`coeFnRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `LocallyConstant` `instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.nonAssocSemiring` `RingHom.instFunLike` `coeFnRingHom` `instFunLike`	—	—
`coeFnₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LocallyConstant` `instAddCommMonoid` `Pi.addCommMonoid` `instModule` `Pi.Function.module` `LinearMap.instFunLike` `coeFnₗ` `instFunLike`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instAdd` `Pi.instAdd`	—	—
`coe_algebraMap` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Pi.semiring` `Function.algebra`	—	—
`coe_charFn` 📖	mathematical	`IsClopen`	`DFunLike.coe` `LocallyConstant` `instFunLike` `charFn` `Set.indicator` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	—
`coe_div` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instDiv` `Pi.instDiv`	—	—
`coe_inv` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instInv` `Pi.instInv`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instMul` `Pi.instMul`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instNeg` `Pi.instNeg`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instOne` `Pi.instOne`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `smul` `Function.hasSMul`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instSub` `Pi.instSub`	—	—
`coe_vadd` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `vadd` `Function.hasVAdd`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instZero` `Pi.instZero`	—	—
`comapAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `LocallyConstant` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `comapAddMonoidHom` `comap`	—	—
`comapMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LocallyConstant` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `comapMonoidHom` `comap`	—	—
`comapRingHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingHom` `instNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `comapRingHom` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`comapₐ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgHom` `instSemiring` `instAlgebra` `AlgHom.funLike` `comapₐ` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`comapₗ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `comapₗ` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`congrLeftRingEquiv_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingEquiv` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `congrLeftRingEquiv` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	—
`congrLeftRingEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingEquiv` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `congrLeftRingEquiv` `Homeomorph` `Homeomorph.instEquivLike`	—	—
`congrLeftₐ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgEquiv` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `congrLeftₐ` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	—
`congrLeftₐ_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgEquiv` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `congrLeftₐ` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	—
`congrLeftₗ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `congrLeftₗ` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	`RingHomInvPair.ids`
`congrLeftₗ_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `congrLeftₗ` `Homeomorph` `Homeomorph.instEquivLike`	—	`RingHomInvPair.ids`
`congrRightRingEquiv_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingEquiv` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `congrRightRingEquiv`	—	—
`congrRightRingEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingEquiv` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `congrRightRingEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `EquivLike.toEquiv`	—	—
`congrRightₐ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgEquiv` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `congrRightₐ` `EquivLike.toFunLike` `AlgEquiv.instEquivLike`	—	—
`congrRightₐ_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgEquiv` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `congrRightₐ` `EquivLike.toFunLike` `AlgEquiv.instEquivLike`	—	—
`congrRightₗ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `congrRightₗ`	—	`RingHomInvPair.ids`
`congrRightₗ_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `congrRightₗ`	—	`RingHomInvPair.ids`
`constAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `LocallyConstant` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `constAddMonoidHom` `const`	—	—
`constMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LocallyConstant` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `constMonoidHom` `const`	—	—
`constRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `LocallyConstant` `instNonAssocSemiring` `RingHom.instFunLike` `constRingHom` `const`	—	—
`constₐ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgHom` `instSemiring` `instAlgebra` `AlgHom.funLike` `constₐ`	—	—
`constₗ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `constₗ`	—	—
`div_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instDiv`	—	—
`evalAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `LocallyConstant` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `evalAddMonoidHom` `instFunLike`	—	—
`evalMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LocallyConstant` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `evalMonoidHom` `instFunLike`	—	—
`evalRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `LocallyConstant` `instNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `evalRingHom` `instFunLike`	—	—
`evalₐ_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `LocallyConstant` `instSemiring` `instAlgebra` `AlgHom.funLike` `evalₐ` `instFunLike`	—	—
`evalₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LocallyConstant` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `evalₗ` `instFunLike`	—	—
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instInv`	—	—
`ker_comapₗ` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`LinearMap.ker` `LocallyConstant` `instAddCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `comapₗ` `Bot.bot` `Submodule` `Submodule.instBot`	—	`LinearMap.ker_eq_bot_of_injective` `comap_injective`
`mapAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `LocallyConstant` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `mapAddMonoidHom` `map`	—	—
`mapMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LocallyConstant` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `mapMonoidHom` `map`	—	—
`mapRingHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `RingHom` `instNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `mapRingHom`	—	—
`mapₐ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `AlgHom` `instSemiring` `instAlgebra` `AlgHom.funLike` `mapₐ`	—	—
`mapₗ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `mapₗ`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instMul`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instNeg`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instOne`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `smul`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instSub`	—	—
`vadd_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `vadd`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `instFunLike` `instZero`	—	—

---

← Back to Index