Documentation Verification Report

AsTensorProduct

📁 Source: Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

Statistics

Metric	Count
Definitions `ofTensorProduct`, `ofTensorProductEquivOfFiniteNoetherian`, `ofTensorProductEquivOfPiFintype`	3
Theorems `coe_ofTensorProductEquivOfFiniteNoetherian`, `flat_of_isNoetherian`, `ofTensorProductEquivOfFiniteNoetherian_apply`, `ofTensorProductEquivOfFiniteNoetherian_symm_of`, `ofTensorProduct_bijective_of_finite_of_isNoetherian`, `ofTensorProduct_bijective_of_pi_of_fintype`, `ofTensorProduct_naturality`, `ofTensorProduct_surjective_of_finite`, `ofTensorProduct_tmul`, `tensor_map_id_left_eq_map`, `tensor_map_id_left_injective_of_injective`	11
Total	14

AdicCompletion

Definitions

Name	Category	Theorems
`ofTensorProduct` 📖	CompOp	7 math math: `ofTensorProduct_surjective_of_finite`, `coe_ofTensorProductEquivOfFiniteNoetherian`, `ofTensorProduct_bijective_of_finite_of_isNoetherian`, `ofTensorProduct_bijective_of_pi_of_fintype`, `ofTensorProduct_tmul`, `ofTensorProductEquivOfFiniteNoetherian_apply`, `ofTensorProduct_naturality`
`ofTensorProductEquivOfFiniteNoetherian` 📖	CompOp	4 math math: `coe_ofTensorProductEquivOfFiniteNoetherian`, `ofTensorProductEquivOfFiniteNoetherian_symm_of`, `tensor_map_id_left_eq_map`, `ofTensorProductEquivOfFiniteNoetherian_apply`
`ofTensorProductEquivOfPiFintype` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofTensorProductEquivOfFiniteNoetherian` 📖	mathematical	—	`LinearEquiv.toLinearMap` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `ofTensorProductEquivOfFiniteNoetherian` `ofTensorProduct`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `RingHomInvPair.ids`
`flat_of_isNoetherian` 📖	mathematical	—	`Module.Flat` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `Module.Flat.iff_lTensor_injective'` `tensor_map_id_left_injective_of_injective` `Module.instFiniteSubtypeMemIdealOfIsNoetherian` `Module.Finite.self` `Submodule.injective_subtype`
`ofTensorProductEquivOfFiniteNoetherian_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `ofTensorProductEquivOfFiniteNoetherian` `LinearMap` `LinearMap.instFunLike` `ofTensorProduct`	—	`IsScalarTower.right` `RingHomInvPair.ids` `Algebra.to_smulCommClass`
`ofTensorProductEquivOfFiniteNoetherian_symm_of` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `instAddCommGroup` `TensorProduct.addCommMonoid` `module` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `instAlgebra` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `ofTensorProductEquivOfFiniteNoetherian` `LinearMap` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `of` `TensorProduct.tmul` `instOne`	—	`IsScalarTower.left` `RingHomInvPair.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `ofTensorProduct_tmul` `one_smul` `LinearEquiv.symm_apply_apply`
`ofTensorProduct_bijective_of_finite_of_isNoetherian` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `LinearMap.instFunLike` `ofTensorProduct`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `Module.Finite.exists_fin'` `Finite.of_fintype`
`ofTensorProduct_bijective_of_pi_of_fintype` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `LinearMap.instFunLike` `ofTensorProduct`	—	`nonempty_fintype` `IsScalarTower.right` `Algebra.to_smulCommClass` `EquivLike.bijective` `RingHomInvPair.ids`
`ofTensorProduct_naturality` 📖	mathematical	—	`LinearMap.comp` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `map` `ofTensorProduct` `IsScalarTower.to_smulCommClass` `TensorProduct.AlgebraTensorModule.map` `LinearMap.id`	—	`TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.right` `IsScalarTower.left` `instIsScalarTower_1` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass` `LinearMap.ext_ring` `LinearMap.ext` `ext` `ofTensorProduct_tmul` `one_smul`
`ofTensorProduct_surjective_of_finite` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `LinearMap.instFunLike` `ofTensorProduct`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `Module.Finite.exists_fin'` `RingHomCompTriple.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `instIsScalarTower_1` `LinearMap.ext_ring` `IsScalarTower.to_smulCommClass` `LinearMap.pi_ext'` `Finite.of_fintype` `ext` `ofTensorProduct_tmul` `one_smul` `map_surjective` `Function.Bijective.surjective` `ofTensorProduct_bijective_of_pi_of_fintype` `Function.Surjective.of_comp`
`ofTensorProduct_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `module` `Algebra.to_smulCommClass` `instAlgebra` `LinearMap.instFunLike` `ofTensorProduct` `TensorProduct.tmul` `smul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `of`	—	`IsScalarTower.left`
`tensor_map_id_left_eq_map` 📖	mathematical	—	`TensorProduct.AlgebraTensorModule.map` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `instAlgebra` `Algebra.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instModuleOfIsScalarTower` `Algebra.toSMul` `IsScalarTower.right` `module` `AddCommGroup.toAddCommMonoid` `LinearMap.id` `LinearMap.comp` `TensorProduct` `TensorProduct.addCommMonoid` `instAddCommGroup` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `ofTensorProductEquivOfFiniteNoetherian` `map`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `coe_ofTensorProductEquivOfFiniteNoetherian` `ofTensorProduct_naturality` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower_left` `LinearMap.ext_ring` `LinearMap.ext` `IsScalarTower.left` `ofTensorProduct_tmul` `one_smul` `ofTensorProductEquivOfFiniteNoetherian_symm_of`
`tensor_map_id_left_injective_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`TensorProduct` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `module` `IsScalarTower.to_smulCommClass` `instAlgebra` `TensorProduct.AlgebraTensorModule.map` `LinearMap.id`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `tensor_map_id_left_eq_map` `EquivLike.toEmbeddingLike` `map_injective`

---

← Back to Index