FreeLocus

📁 Source: Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean

Statistics

Metric	Count
Definitions `freeLocus`, `rankAtStalk`	2
Theorems `basicOpen_subset_freeLocus_iff`, `comap_freeLocus_le`, `freeLocus_congr`, `freeLocus_eq_univ`, `freeLocus_eq_univ_iff`, `freeLocus_localization`, `isLocallyConstant_rankAtStalk`, `isLocallyConstant_rankAtStalk_freeLocus`, `isOpen_freeLocus`, `mem_freeLocus`, `mem_freeLocus_iff_tensor`, `mem_freeLocus_of_isLocalization`, `nontrivial_of_rankAtStalk_pos`, `rankAtStalk_baseChange`, `rankAtStalk_eq`, `rankAtStalk_eq_finrank_of_free`, `rankAtStalk_eq_finrank_tensorProduct`, `rankAtStalk_eq_of_equiv`, `rankAtStalk_eq_zero_iff_notMem_support`, `rankAtStalk_eq_zero_iff_subsingleton`, `rankAtStalk_eq_zero_of_subsingleton`, `rankAtStalk_pi`, `rankAtStalk_pos_iff_mem_support`, `rankAtStalk_prod`, `rankAtStalk_self`, `rankAtStalk_tensorProduct`, `rankAtStalk_tensorProduct_of_isScalarTower`	27
Total	29

Module

Definitions

Name	Category	Theorems
`freeLocus` 📖	CompOp	12 math math: `freeLocus_localization`, `freeLocus_eq_univ`, `basicOpen_subset_freeLocus_iff`, `comap_freeLocus_le`, `freeLocus_congr`, `freeLocus_eq_univ_iff`, `isOpen_freeLocus`, `isLocallyConstant_rankAtStalk_freeLocus`, `mem_freeLocus_iff_tensor`, `mem_freeLocus_of_isLocalization`, `mem_freeLocus`, `Algebra.smoothLocus_eq_compl_support_inter`
`rankAtStalk` 📖	CompOp	17 math math: `rankAtStalk_eq`, `rankAtStalk_eq_zero_iff_notMem_support`, `Grassmannian.rankAtStalk_eq`, `rankAtStalk_pi`, `rankAtStalk_baseChange`, `rankAtStalk_eq_of_equiv`, `rankAtStalk_eq_zero_iff_subsingleton`, `rankAtStalk_eq_finrank_tensorProduct`, `rankAtStalk_tensorProduct`, `rankAtStalk_tensorProduct_of_isScalarTower`, `isLocallyConstant_rankAtStalk_freeLocus`, `rankAtStalk_pos_iff_mem_support`, `rankAtStalk_prod`, `isLocallyConstant_rankAtStalk`, `rankAtStalk_eq_zero_of_subsingleton`, `rankAtStalk_self`, `rankAtStalk_eq_finrank_of_free`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basicOpen_subset_freeLocus_iff` 📖	mathematical	—	`Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Opens` `PrimeSpectrum.zariskiTopology` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.basicOpen` `freeLocus` `Projective` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instSemiring` `Ring.toSemiring` `CommRing.toRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `LocalizedModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommSemiring.toCommMonoid` `toDistribMulAction` `OreLocalization.instModule`	—	`freeLocus_eq_univ_iff` `instFinitePresentationLocalizationLocalizedModule` `freeLocus_localization` `Set.preimage_eq_univ_iff` `PrimeSpectrum.localization_away_comap_range` `Localization.isLocalization`
`comap_freeLocus_le` 📖	mathematical	—	`Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instLE` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring` `freeLocus` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	`PrimeSpectrum.isPrime` `Algebra.to_smulCommClass` `mem_freeLocus_iff_tensor` `Localization.isLocalization` `IsScalarTower.right` `IsScalarTower.of_algebraMap_eq'` `RingHom.instRingHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsLocalization.map_comp` `OreLocalization.instIsScalarTower` `RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids` `Free.of_equiv` `Algebra.TensorProduct.instFree` `Set.mem_preimage`
`freeLocus_congr` 📖	mathematical	—	`freeLocus`	—	`RingHomInvPair.ids` `Set.ext` `mem_freeLocus_of_isLocalization` `PrimeSpectrum.isPrime` `Localization.isLocalization` `IsScalarTower.left` `IsScalarTower.right` `RingHomCompTriple.ids` `IsLocalizedModule.of_linearEquiv_right` `localizedModuleIsLocalizedModule` `OreLocalization.instIsScalarTower_1`
`freeLocus_eq_univ` 📖	mathematical	—	`freeLocus` `Set.univ` `PrimeSpectrum` `CommRing.toCommSemiring`	—	`PrimeSpectrum.isPrime` `free_of_flat_of_isLocalRing` `Localization.AtPrime.isLocalRing` `Finite.instLocalizationLocalizedModule` `Flat.localizedModule`
`freeLocus_eq_univ_iff` 📖	mathematical	—	`freeLocus` `Set.univ` `PrimeSpectrum` `CommRing.toCommSemiring` `Projective` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`PrimeSpectrum.isPrime` `projective_of_localization_maximal` `Ideal.IsMaximal.isPrime` `Projective.of_free` `Ideal.IsMaximal.isPrime'` `free_of_flat_of_isLocalRing` `Localization.AtPrime.isLocalRing` `Finite.instLocalizationLocalizedModule` `instFiniteOfFinitePresentation` `Flat.localizedModule` `Flat.of_projective`
`freeLocus_localization` 📖	mathematical	—	`freeLocus` `Localization` `CommRing.toCommMonoid` `LocalizedModule` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `OreLocalization.instAddCommGroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommSemiring.toCommMonoid` `toDistribMulAction` `OreLocalization.instModule` `Set.preimage` `PrimeSpectrum` `PrimeSpectrum.comap` `algebraMap` `OreLocalization.instAlgebra` `Algebra.id`	—	`Set.ext` `RingHom.instRingHomClass` `Ideal.IsPrime.under` `PrimeSpectrum.isPrime` `Ideal.IsPrime.ne_top` `Ideal.eq_top_of_isUnit_mem` `IsLocalization.map_units` `Localization.isLocalization` `IsScalarTower.right` `IsLocalization.localization_isScalarTower_of_submonoid_le` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsLocalization.isLocalization_of_submonoid_le` `IsLocalization.isLocalization_of_is_exists_mul_mem` `IsLocalization.exists_mk'_eq` `IsLocalization.mk'_eq_mul_mk'_one` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `IsLocalization.mk'_spec'` `IsScalarTower.left` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `SemigroupAction.mul_smul` `algebraMap_smul` `OreLocalization.instIsScalarTower_1` `localizedModuleIsLocalizedModule` `LinearMap.IsScalarTower.compatibleSMul` `IsLocalizedModule.instLiftOfLE` `IsLocalizedModule.of_restrictScalars` `IsLocalizedModule.of_exists_mul_mem` `mem_freeLocus_of_isLocalization`
`isLocallyConstant_rankAtStalk` 📖	mathematical	—	`IsLocallyConstant` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `rankAtStalk`	—	`freeLocus_eq_univ` `instFiniteOfFinitePresentation` `IsLocallyConstant.comp_continuous` `isLocallyConstant_rankAtStalk_freeLocus` `Homeomorph.continuous`
`isLocallyConstant_rankAtStalk_freeLocus` 📖	mathematical	—	`IsLocallyConstant` `Set.Elem` `PrimeSpectrum` `CommRing.toCommSemiring` `freeLocus` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `PrimeSpectrum.zariskiTopology` `rankAtStalk`	—	`IsLocallyConstant.iff_exists_open` `PrimeSpectrum.isPrime` `FinitePresentation.exists_free_localizedModule_powers` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `OreLocalization.instIsScalarTower_1` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Localization.isLocalization` `IsOpen.preimage` `continuous_subtype_val` `TopologicalSpace.Opens.is_open'` `Ideal.one_notMem` `IsLocalization.localization_isScalarTower_of_submonoid_le` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `SemigroupAction.mul_smul` `algebraMap_smul` `IsLocalization.isLocalization_of_submonoid_le` `LinearMap.IsScalarTower.compatibleSMul` `IsLocalizedModule.instLiftOfLE` `IsLocalizedModule.of_restrictScalars` `finrank_of_isLocalizedModule_of_free`
`isOpen_freeLocus` 📖	mathematical	—	`IsOpen` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `freeLocus`	—	`isOpen_iff_forall_mem_open` `PrimeSpectrum.isPrime` `FinitePresentation.exists_free_localizedModule_powers` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `OreLocalization.instIsScalarTower_1` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Localization.isLocalization` `basicOpen_subset_freeLocus_iff` `Projective.of_free` `TopologicalSpace.Opens.is_open'`
`mem_freeLocus` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `freeLocus` `Free` `Localization.AtPrime` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `LocalizedModule` `Ideal.primeCompl` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `OreLocalization.instSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction` `OreLocalization.instModule`	—	—
`mem_freeLocus_iff_tensor` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `freeLocus` `Free` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	`PrimeSpectrum.isPrime` `mem_freeLocus_of_isLocalization` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsLocalization.tensorProduct_isLocalizedModule` `Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right`
`mem_freeLocus_of_isLocalization` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `freeLocus` `Free` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`PrimeSpectrum.isPrime` `Free.iff_of_ringEquiv` `Localization.isLocalization` `RingHomInvPair.ids` `IsScalarTower.left` `IsScalarTower.right` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHomInvPair.of_ringEquiv` `IsLocalization.exists_mk'_eq` `smulCommClass_self` `End.isUnit_iff` `IsLocalizedModule.map_units` `IsLocalization.map_id_mk'` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `OreLocalization.instIsScalarTower_1` `IsLocalization.smul_mk'_self` `algebraMap_smul` `LinearEquiv.left_inv` `LinearEquiv.right_inv`
`nontrivial_of_rankAtStalk_pos` 📖	mathematical	`Preorder.toLT` `Pi.preorder` `PrimeSpectrum` `CommRing.toCommSemiring` `Nat.instPreorder` `Pi.instZero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `rankAtStalk`	`Nontrivial`	—	`rankAtStalk_eq_zero_of_subsingleton`
`rankAtStalk_baseChange` 📖	mathematical	—	`rankAtStalk` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `PrimeSpectrum.comap` `algebraMap`	—	`PrimeSpectrum.isPrime` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `PrimeSpectrum.instLiesOverAsIdealComapAlgebraMap` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHomCompTriple.ids` `OreLocalization.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `rankAtStalk.eq_1` `LinearEquiv.finrank_eq` `finrank_baseChange` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `free_of_flat_of_isLocalRing` `Finite.instLocalizationLocalizedModule` `Flat.localizedModule`
`rankAtStalk_eq` 📖	mathematical	—	`rankAtStalk` `finrank` `Ideal.ResidueField` `PrimeSpectrum.asIdeal` `CommRing.toCommSemiring` `PrimeSpectrum.isPrime` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `IsLocalRing.ResidueField`	—	`PrimeSpectrum.isPrime` `RingHomInvPair.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `IsLocalRing.instIsScalarTowerResidueField` `LinearEquiv.finrank_eq` `finrank_baseChange` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Localization.AtPrime.isLocalRing` `free_of_flat_of_isLocalRing` `Finite.base_change` `Flat.baseChange` `rankAtStalk_eq_finrank_tensorProduct`
`rankAtStalk_eq_finrank_of_free` 📖	mathematical	—	`rankAtStalk` `Pi.instNatCast` `PrimeSpectrum` `CommRing.toCommSemiring` `finrank` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`PrimeSpectrum.isPrime` `IsScalarTower.left` `IsScalarTower.right` `finrank_of_isLocalizedModule_of_free` `localizedModuleIsLocalizedModule` `OreLocalization.instIsScalarTower_1` `Localization.isLocalization` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing`
`rankAtStalk_eq_finrank_tensorProduct` 📖	mathematical	—	`rankAtStalk` `finrank` `Localization.AtPrime` `CommRing.toCommSemiring` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `TensorProduct` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toDistribMulAction` `Semiring.toModule` `AddCommGroup.toAddCommMonoid` `OreLocalization.instModuleOfIsScalarTower` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsScalarTower.right` `Algebra.id` `OreLocalization.instSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `OreLocalization.instModule` `Algebra.to_smulCommClass` `OreLocalization.instAlgebra`	—	`PrimeSpectrum.isPrime` `RingHomInvPair.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `rankAtStalk.eq_1` `LinearEquiv.finrank_eq`
`rankAtStalk_eq_of_equiv` 📖	mathematical	—	`rankAtStalk`	—	`RingHomInvPair.ids` `LinearEquiv.finrank_eq` `PrimeSpectrum.isPrime` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `OreLocalization.instIsScalarTower_1` `Localization.isLocalization`
`rankAtStalk_eq_zero_iff_notMem_support` 📖	mathematical	—	`rankAtStalk` `PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support`	—	`PrimeSpectrum.isPrime` `notMem_support_iff` `subsingleton_of_rank_zero` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `free_of_flat_of_isLocalRing` `Finite.instLocalizationLocalizedModule` `Flat.localizedModule` `CharP.cast_eq_zero` `CharP.ofCharZero` `Cardinal.instCharZero` `finrank_zero_of_subsingleton`
`rankAtStalk_eq_zero_iff_subsingleton` 📖	mathematical	—	`rankAtStalk` `Pi.instZero` `PrimeSpectrum` `CommRing.toCommSemiring` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`support_eq_empty_iff` `rankAtStalk_eq_zero_iff_notMem_support` `Pi.zero_apply` `rankAtStalk_eq_zero_of_subsingleton`
`rankAtStalk_eq_zero_of_subsingleton` 📖	mathematical	—	`rankAtStalk` `Pi.instZero` `PrimeSpectrum` `CommRing.toCommSemiring` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`finrank_zero_of_subsingleton` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `LocalizedModule.instSubsingleton`
`rankAtStalk_pi` 📖	mathematical	`Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Finite` `CommSemiring.toSemiring`	`rankAtStalk` `Pi.addCommGroup` `Pi.module` `finsum` `Nat.instAddCommMonoid`	—	`nonempty_fintype` `PrimeSpectrum.isPrime` `IsScalarTower.left` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Localization.isLocalization` `OreLocalization.instIsScalarTower_1` `Pi.isScalarTower` `localizedModuleIsLocalizedModule` `IsLocalizedModule.pi` `free_of_flat_of_isLocalRing` `Localization.AtPrime.isLocalRing` `Finite.instLocalizationLocalizedModule` `Flat.localizedModule` `LinearEquiv.finrank_eq` `finrank_pi_fintype` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `finsum_eq_sum_of_fintype`
`rankAtStalk_pos_iff_mem_support` 📖	mathematical	—	`rankAtStalk` `PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `support`	—	`Iff.not_left` `rankAtStalk_eq_zero_iff_notMem_support`
`rankAtStalk_prod` 📖	mathematical	—	`rankAtStalk` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Pi.instAdd` `PrimeSpectrum`	—	`PrimeSpectrum.isPrime` `RingHomInvPair.ids` `Localization.isLocalization` `IsScalarTower.left` `IsScalarTower.right` `OreLocalization.instIsScalarTower_1` `Prod.isScalarTower` `localizedModuleIsLocalizedModule` `IsLocalizedModule.prodMap` `LinearEquiv.finrank_eq` `finrank_prod` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `free_of_flat_of_isLocalRing` `Finite.instLocalizationLocalizedModule` `Flat.localizedModule`
`rankAtStalk_self` 📖	mathematical	—	`rankAtStalk` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.instOne` `PrimeSpectrum` `Nat.instOne`	—	`rankAtStalk_eq_finrank_of_free` `Free.self` `finrank_self` `commRing_strongRankCondition` `Nat.cast_one`
`rankAtStalk_tensorProduct` 📖	mathematical	—	`rankAtStalk` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.instModule` `Pi.instMul` `PrimeSpectrum`	—	`PrimeSpectrum.isPrime` `RingHomInvPair.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `OreLocalization.instIsScalarTower` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids` `IsScalarTower.left` `TensorProduct.isScalarTower_left` `rankAtStalk_eq_finrank_tensorProduct` `LinearEquiv.finrank_eq` `finrank_tensorProduct` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `free_of_flat_of_isLocalRing` `Finite.base_change` `Flat.baseChange` `Pi.mul_apply`
`rankAtStalk_tensorProduct_of_isScalarTower` 📖	mathematical	—	`rankAtStalk` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.leftModule` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass` `PrimeSpectrum.comap` `algebraMap`	—	`IsScalarTower.to_smulCommClass` `Algebra.to_smulCommClass` `smulCommClass_self` `rankAtStalk_eq_of_equiv` `RingHomInvPair.ids` `IsScalarTower.left` `rankAtStalk_tensorProduct` `Finite.base_change` `Flat.baseChange` `rankAtStalk_baseChange`

---

← Back to Index