Documentation Verification Report

Finite

📁 Source: Mathlib/RingTheory/Unramified/Finite.lean

Statistics

Metric	Count
Definitions `elem`, `sec`	2
Theorems `comp_sec`, `finite_of_free`, `finite_of_free_aux`, `flat_of_restrictScalars`, `iff_exists_tensorProduct`, `lmul_elem`, `one_tmul_mul_elem`, `one_tmul_sub_tmul_one_mul_elem`, `projective_of_restrictScalars`	9
Total	11

Algebra.FormallyUnramified

Definitions

Name	Category	Theorems
`elem` 📖	CompOp	3 math math: `one_tmul_mul_elem`, `lmul_elem`, `one_tmul_sub_tmul_one_mul_elem`
`sec` 📖	CompOp	1 math math: `comp_sec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_sec` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Algebra.id` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHom.id` `RingHomCompTriple.ids` `TensorProduct.AlgebraTensorModule.lift` `LinearMap.flip` `IsScalarTower.to_smulCommClass'` `LinearMap.restrictScalars` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `LinearMap.IsScalarTower.compatibleSMul` `Algebra.toSMul` `LinearMap.instIsScalarTower` `AlgHom.toLinearMap` `Module.End` `Module.End.instSemiring` `Module.End.instAlgebra` `Algebra.lsmul` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `sec` `LinearMap.id`	—	`LinearMap.ext` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass'` `SMulCommClass.symm` `IsScalarTower.left` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.instIsScalarTower` `smulCommClass_self` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `MonoidWithZeroHomClass.toZeroHomClass` `Algebra.to_smulCommClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `zero_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemigroupAction.mul_smul` `SMulCommClass.smul_comm` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `add_smul` `lmul_elem` `one_smul`
`finite_of_free` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHomInvPair.ids` `Module.Basis.linearCombination_repr` `Finsupp.linearCombination_apply` `LinearEquiv.trans.congr_simp` `Finsupp.lcongr_symm` `Module.Basis.coe_reindex` `Finsupp.coe_basisSingleOne` `Finsupp.lcongr_single` `finsuppTensorFinsupp_symm_single` `Module.Basis.repr_symm_apply` `Module.Basis.coe_singleton` `Finsupp.linearCombination_single` `mul_one` `one_smul` `top_le_iff` `not_imp_comm` `Finsupp.notMem_support_iff` `MulZeroClass.mul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finset.sum_congr` `zero_smul` `Finset.sum_const_zero` `Equiv.injective` `LinearEquiv.injective` `IsScalarTower.left` `Finsupp.onFinset_sum` `Algebra.to_smulCommClass` `Finset.mul_sum` `one_mul` `one_tmul_mul_elem` `finite_of_free_aux` `Finsupp.sum_equivMapDomain` `Finsupp.sum_uncurry_index` `Module.Basis.tensorProduct_apply` `DFunLike.congr_fun` `lmul_elem` `map_finsuppSum` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finsupp.sum.eq_1` `Finset.coe_image₂` `Finset.sum_mul` `smul_mul_assoc` `Submodule.sum_mem` `Submodule.smul_mem` `Submodule.subset_span`
`finite_of_free_aux` 📖	mathematical	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Module.Basis` `Module.Basis.instFunLike`	`TensorProduct` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finsupp.sum` `TensorProduct.addCommMonoid` `Finset.sum` `Finset.biUnion` `Finsupp.support` `Algebra.toSMul` `Finsupp.instFunLike` `TensorProduct.instSMul`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `IsScalarTower.right` `Finsupp.sum.eq_1` `Finset.mul_sum` `one_mul` `mul_comm` `Module.Basis.linearCombination_repr` `Finset.sum_congr` `TensorProduct.tmul_sum` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `Finsupp.sum_sum_index` `zero_smul` `add_smul` `Finsupp.sum_smul_index` `SemigroupAction.mul_smul` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finset.sum_comm` `Finset.sum_subset_zero_on_sdiff` `Finset.subset_biUnion_of_mem` `TensorProduct.zero_tmul`
`flat_of_restrictScalars` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.Flat.of_retract` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `Module.Flat.baseChange` `IsScalarTower.to_smulCommClass'` `SMulCommClass.symm` `IsScalarTower.left` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.instIsScalarTower` `smulCommClass_self` `comp_sec`
`iff_exists_tensorProduct` 📖	mathematical	—	`Algebra.FormallyUnramified` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.TensorProduct.instRing` `CommRing.toRing` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `TensorProduct.zero` `DFunLike.coe` `AlgHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `Algebra.TensorProduct.lmul'`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Algebra.formallyUnramified_iff` `KaehlerDifferential.eq_1` `Ideal.cotangent_subsingleton_iff` `Ideal.isIdempotentElem_iff_of_fg` `KaehlerDifferential.ideal_fg` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Ideal.mem_span_singleton` `Ideal.subset_span` `mul_comm` `mul_assoc` `sub_mul` `one_mul` `IsIdempotentElem.eq` `sub_self` `MulZeroClass.zero_mul` `sub_sub_cancel` `dvd_refl` `sub_sub_self` `mul_sub` `mul_one` `le_antisymm` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add`
`lmul_elem` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `Algebra.TensorProduct.lmul'` `elem` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `iff_exists_tensorProduct`
`one_tmul_mul_elem` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `elem`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `sub_eq_zero` `sub_mul` `one_tmul_sub_tmul_one_mul_elem`
`one_tmul_sub_tmul_one_mul_elem` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.TensorProduct.instRing` `CommRing.toRing` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `elem` `TensorProduct.zero`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `iff_exists_tensorProduct`
`projective_of_restrictScalars` 📖	mathematical	—	`Module.Projective` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.Projective.of_split` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `Module.Projective.tensorProduct` `Module.Projective.of_free` `Module.Free.self` `IsScalarTower.to_smulCommClass'` `SMulCommClass.symm` `IsScalarTower.left` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.instIsScalarTower` `smulCommClass_self` `comp_sec`

---

← Back to Index