Main results 1 to 100

Declaration	Kind	Where	Note
Module.Baer.of_isSemisimpleRing	theorem	ProjectiveModules/Module/FiniteConsistency.lean, line 41	Every left module over a semisimple ring satisfies Baer's ideal-extension criterion, with independent scalar and target universes.
Module.Baer.exists_solution_of_finite	theorem	ProjectiveModules/Module/FiniteConsistency.lean, line 54	For a ring and a left module satisfying Module.Baer, a row-finite linear system has a full solution if every finite set of rows does. The finite assignments need not be compatible. Solutions are arbitrary functions on the coordinate type; all four universes are independent.
Finsupp.exists_solution_iff_finite	theorem	ProjectiveModules/Module/FiniteConsistency.lean, line 109	Over a semisimple ring, full solvability and finite consistency are equivalent for every left module. Existing instances cover division rings, without countability, dimension or nontriviality restrictions.
LinearMap.injective_of_lTensor_injective_of_eval_injective	theorem	ProjectiveModules/Dual/TensorProduct.lean, line 518	Tensoring with a module with faithful scalar action reflects injectivity for maps whose domain has injective canonical dual evaluation, over a commutative semiring with additive commutative monoids and independent scalar/carrier universes. No flatness or finite generation is assumed.
LinearMap.injective_of_lTensor_injective_of_projective	theorem	ProjectiveModules/Dual/TensorProduct.lean, line 535	Projective-source specialization using Mathlib's existing dual-evaluation injectivity theorem, with arbitrary rank and unrestricted codomain.
linearIndependent_of_injective_sum_tmul	theorem	ProjectiveModules/Dual/TensorProduct.lean, line 552	Injectivity of the tensor-valued finite-support relation map with coefficients in a module with faithful scalar action implies linear independence of the original arbitrarily indexed family. No flatness or finite-index assumption is required.
LinearMap.traceOfFiniteProjective	def	ProjectiveModules/Module/Trace/Basic.lean, line 43	Linear contraction trace over a commutative semiring, for finite projective additive-commutative-monoid modules; no freeness or additive inverses.
LinearMap.traceOfFiniteProjective_smulRight	theorem	ProjectiveModules/Module/Trace/Basic.lean, line 59	Rank-one evaluation sends the endomorphism m ↦ φ m • x to φ x.
LinearMap.partialTraceOfFiniteProjective	def	ProjectiveModules/Module/Trace/Partial.lean, line 65	Canonical linear partial trace on all maps M tensor N → M tensor P over a commutative semiring. Only the traced factor M is finite projective; N and P are arbitrary additive-commutative-monoid modules, with independent scalar and three carrier universes.
LinearMap.partialTraceOfFiniteProjective_apply	theorem	ProjectiveModules/Module/Trace/Partial.lean, line 77	At every input n, contract the inverse tensor–Hom image of m ↦ f(m tensor n) by tensoring the scalar finite-projective trace with the identity of P and applying the left unitor.
LinearMap.partialTraceOfFiniteProjective_tensorProduct	theorem	ProjectiveModules/Module/Trace/Partial.lean, line 88	The partial trace of TensorProduct.map a b is traceOfFiniteProjective R M a • b. This is the ordinary unnormalized trace, with no finiteness or projectivity assumption on the source or target of b.
LinearMap.traceOfFiniteProjective_conj	theorem	ProjectiveModules/Module/Trace/Conjugation.lean, line 36	Invariance under linear equivalence between finite projective carriers in independent universes.
LinearMap.traceOfFiniteProjective_dualMap	theorem	ProjectiveModules/Module/Trace/Dual.lean, line 34	The trace of the dual endomorphism equals the trace of the original endomorphism for finite projective modules over a commutative semiring, with independent scalar and carrier universes and the pointwise dual action.
LinearMap.traceOfFiniteProjective_eq_trace	theorem	ProjectiveModules/Module/Trace/Comparison.lean, line 65	Finite-free semiring comparison with Mathlib's finite-basis trace; not a universal assertion for nonfree projectives.
LinearMap.traceOfFiniteProjective_restrictScalars	theorem	ProjectiveModules/Module/Trace/ScalarRestriction.lean, line 52	For a commutative-semiring algebra R → A with A finite projective over R and an additive-commutative-monoid module M finite projective over A, the R-trace of any A-linear endomorphism f restricted to R equals the R-trace of multiplication on A by its A-trace. The given R-action on M is compatible with the tower. Finiteness and projectivity over R are supplied explicitly by Module.Finite.trans and Module.Projective.trans, not additional hypotheses. Scalar and carrier universes are independent; no freeness or additive inverses are required.
LinearMap.traceOfFiniteProjective_restrictScalars_lmul_iff_trace_trace	theorem	ProjectiveModules/Module/Trace/ScalarRestriction.lean, line 92	For a tower R → A → T of commutative rings, with A finite free over R and T finite free over A, the finite-projective restriction identity for A-linear multiplication by x is equivalent to Algebra.trace R T x = Algebra.trace R A (Algebra.trace A T x), the symmetric form of Mathlib's Algebra.trace_trace. Scalar universes are independent; freeness and finiteness over R are derived from the two successive extensions, not separately assumed for T.
LinearMap.traceOfFiniteProjective_baseChange	theorem	ProjectiveModules/Module/Trace/BaseChange.lean, line 45	Contraction trace commutes with arbitrary scalar extension between commutative semirings: the trace of f.baseChange A on A tensor M is the algebraMap image of the trace of f. Only the source module is assumed finite projective; scalar and carrier universes are independent, with no freeness, flatness or finiteness assumption on the scalar extension.
LinearMap.traceOfFiniteProjective_baseChange_iff_trace	theorem	ProjectiveModules/Module/Trace/BaseChange.lean, line 72	Over commutative rings and a finite free source, source and target contraction-trace comparisons identify the scalar-extension identity with Mathlib's LinearMap.trace_baseChange formula.
LinearMap.traceOfFiniteProjective_prodMap	theorem	ProjectiveModules/Module/Trace/Prod.lean, line 101	Product endomorphisms have the sum of the factor traces over a commutative semiring, with independent scalar and factor universes.
LinearMap.traceOfFiniteProjective_inl_fst	theorem	ProjectiveModules/Module/Trace/Prod.lean, line 113	The first diagonal inclusion-projection block has the trace of its factor endomorphism.
LinearMap.traceOfFiniteProjective_inr_snd	theorem	ProjectiveModules/Module/Trace/Prod.lean, line 126	The second diagonal inclusion-projection block has the trace of its factor endomorphism.
LinearMap.traceOfFiniteProjective_inl_snd	theorem	ProjectiveModules/Module/Trace/Prod.lean, line 156	The upper off-diagonal block has trace zero, assuming finite projectivity only of the product.
LinearMap.traceOfFiniteProjective_inr_fst	theorem	ProjectiveModules/Module/Trace/Prod.lean, line 184	The lower off-diagonal block has trace zero, assuming finite projectivity only of the product.
LinearMap.traceOfFiniteProjective_coprod_prod	theorem	ProjectiveModules/Module/Trace/Prod.lean, line 213	An arbitrary block endomorphism of a product of finite projective factors has the sum of its diagonal traces over a commutative semiring, with independent scalar and factor universes.
Module.Free.right_regular	instance	ProjectiveModules/Module/RightRegular.lean, line 40	The ordinary semiring carrier is free under the canonical opposite-scalar right action; zero semirings are included.
Module.Finite.right_regular	instance	ProjectiveModules/Module/RightRegular.lean, line 45	The same right regular carrier is finitely generated, by transport of the left regular module.
Module.Finite.finrank_repr	theorem	ProjectiveModules/Category/FiniteModuleDimension.lean, line 45	Finite rank is preserved by the chosen ring-universe representative, with independent scalar and carrier universes.
ModuleCat.nonempty_iso_iff_finrank_eq	theorem	ProjectiveModules/Category/FiniteModuleDimension.lean, line 59	Finitely generated free objects over a strong-rank-condition ring are isomorphic exactly when finite ranks agree.
FGModuleCat.nonempty_iso_iff_finrank_eq	theorem	ProjectiveModules/Category/FiniteModuleDimension.lean, line 77	The finite-free isomorphism criterion in the finitely generated module category; division-ring freeness is automatic.
Module.Projective.exists_free_stabilizer	theorem	ProjectiveModules/Module/FiniteStabilization.lean, line 50	For arbitrary rings and arbitrary ambient modules, replace a common finite projective stabilizer by the same standard finite free module; n is existential, with no IBN or module cancellation.
IsBaseChange.toDualBaseChangeOfProjective	def	ProjectiveModules/Dual/BaseChange.lean, line 87	Canonical dual base change for finite projective modules over commutative semirings.
IsBaseChange.contractBaseChangeEquivOfProjective	def	ProjectiveModules/Contraction/BaseChange.lean, line 37	Evaluation/contraction compatibility for finite projectives over commutative rings.
ExteriorAlgebra.equivBaseChange	def	ProjectiveModules/ExteriorAlgebra/BaseChange.lean, line 131	Full exterior-algebra base change over arbitrary commutative rings and modules; no finite, projective, flat or invertible-two assumption. This is not a fixed-degree scalar-extension equivalence.
exteriorPower.prodEquivDirectSum	def	ProjectiveModules/ExteriorPower/DirectSum.lean, line 385	Every-degree binary Sum Formula for arbitrary modules over a commutative ring, with ordered P-before-Q wedge inverse and degree zero included.
exteriorPower.prodEquivDirectSum_naturality	theorem	ProjectiveModules/ExteriorPower/DirectSum.lean, line 482	Naturality for arbitrary linear maps over a fixed commutative base ring.
exteriorPower.instProjective	instance	ProjectiveModules/ExteriorPower/Projective.lean, line 30	Exterior powers preserve projectivity, without finite-generation assumptions.
exteriorPower.determinant	def	ProjectiveModules/ExteriorPower/Determinant.lean, line 48	Scalar determinant construction assuming the chosen exterior power is invertible.
Module.Basis.exteriorPower_determinant_eq_det	theorem	ProjectiveModules/ExteriorPower/Top.lean, line 133	Finite-basis top-exterior action agrees with the determinant, including rank zero.
Module.invertible_iff_finite_projective_rankAtStalk_eq_one	theorem	ProjectiveModules/Invertible/OfRankOne.lean, line 64	Invertibility iff finite projectivity and stalk rank one, with these properties on the right as propositions, not preinstalled hypotheses. The zero ring and empty spectrum are not excluded.
Module.Invertible.toModuleEndRingEquiv	def	ProjectiveModules/Invertible/Endomorphism.lean, line 31	Every endomorphism of an invertible module is uniquely scalar.
Module.Invertible.nonempty_linearEquiv_of_fin_stabilization	theorem	ProjectiveModules/Invertible/StableCancellation.lean, line 55	Finite-free stabilization cancellation between invertible modules only.
Module.Invertible.isModuleTopology	theorem	ProjectiveModules/Invertible/Topology.lean, line 64	The given topology of a Hausdorff invertible topological vector space over a nontrivially normed field is its module topology. Scalar and carrier universes are independent; neither field completeness nor a norm on the vector space is assumed.
ContinuousLinearMap.scalarEndEquiv	def	ProjectiveModules/Invertible/Topology.lean, line 108	Scalar multiplication is a continuous linear equivalence from a nontrivially normed field to the bounded-convergence continuous endomorphisms of a Hausdorff invertible topological vector space. The original topology and independent scalar/carrier universes are retained, with no completeness, norm, input vector, frame or inverse. Forward action, inverse action on every vector, algebraic comparison and agreement with the scalar-field homothety equivalence are provided.
Module.Free.countableFinsuppEquivOfProdFiniteFinsuppEquiv	def	ProjectiveModules/Free/CountableCancellation.lean, line 350	Cancel a finite free summand in countably infinite free coordinates; not arbitrary cancellation.
Module.Free.prodNatFinsuppEquivOfSplit	def	ProjectiveModules/Free/CountableAbsorption.lean, line 152	Countable free absorption of a module given explicit split maps.
Module.Free.rightIdealProdEndNatFinsuppEquiv	def	ProjectiveModules/Free/CountableAbsorption.lean, line 351	Corresponding absorption for complemented right ideals of a countable free endomorphism ring.
RingHom.rankCondition	theorem	ProjectiveModules/Free/InvariantBasisNumber.lean, line 41	Rank condition descends along any unital semiring homomorphism from a target with rank condition, with independent source and target universes; the map need not be injective or surjective.
RingHom.invariantBasisNumber	theorem	ProjectiveModules/Free/InvariantBasisNumber.lean, line 49	Invariant basis number descends along any unital semiring homomorphism from a target with invariant basis number; no rank-condition or injectivity premise is needed.
MonoidAlgebra.linearIndependent_freeMonoid_of	theorem	ProjectiveModules/Free/FreeWordAlgebra.lean, line 143	The letter monomials form a linearly independent family over the left regular module of A = MonoidAlgebra K (FreeMonoid alphabet), for arbitrary Semiring K and independently universed alphabet. Canonical finitely supported linear combinations multiply each polynomial coordinate by its letter on the right; its terminal-word coefficients recover the coordinate. Injective reindexing gives arbitrary independent subfamilies. No Nontrivial, commutativity, centrality or finite-alphabet hypothesis. Trivial coefficients and the empty family are included without implying a nonzero module; repeated letters over nontrivial coefficients need not be independent. This is A-linear independence, not merely K-linearity.
MonoidAlgebra.freeWordPairMap_eq_linearCombination	theorem	ProjectiveModules/Free/FreeWordAlgebra.lean, line 181	The two-letter left-A-linear map equals the canonical finitely supported linear combination after the inverse finite coordinate equivalence. Its distinct-letter injectivity follows by reindexing the general family.
MonoidAlgebra.freeWordPairMap_injective	theorem	ProjectiveModules/Free/FreeWordAlgebra.lean, line 196	Over any Semiring K and any alphabet in an independent universe, distinct letters give an injective left-A-linear map from Fin 2 coordinates to A = MonoidAlgebra K (FreeMonoid alphabet). Right multiplication appends letters, and disjoint final suffixes recover both input coefficients. No Nontrivial, commutativity or finite-alphabet hypothesis; trivial coefficients give singleton modules.
MonoidAlgebra.not_strongRankCondition_freeMonoid	theorem	ProjectiveModules/Free/FreeWordAlgebra.lean, line 213	For distinct letters over arbitrary semiring coefficients, the free-word semiring fails the strong rank condition: transport the pair injection to a Fin 1 codomain and contradict the strong-rank bound 2 ≤ 1. Mathlib's free-algebra contrast is credited there to T. Y. Lam. In the rational-Boolean case, rank condition and invariant basis number follow separately by augmentation; these positive properties are not asserted for every coefficient semiring. This entry asserts neither source correspondence nor whole-book coverage.
MonoidAlgebra.freeMonoidAugmentation	def	ProjectiveModules/Free/FreeWordAugmentation.lean, line 47	Zero-generator ring homomorphism from the free-word semiring to its coefficient semiring. Coefficients may be noncommutative or trivial, and coefficient and alphabet universes are independent. Empty alphabets are allowed; no module action on the coefficient carrier is chosen by this construction.
MonoidAlgebra.freeMonoidAugmentation_single	theorem	ProjectiveModules/Free/FreeWordAugmentation.lean, line 62	A monomial maps to its coefficient multiplied by the value of its word under the zero-generator word map.
MonoidAlgebra.freeMonoidAugmentation_single_one	theorem	ProjectiveModules/Free/FreeWordAugmentation.lean, line 68	Constant monomials map to their coefficients.
MonoidAlgebra.freeMonoidAugmentation_single_of	theorem	ProjectiveModules/Free/FreeWordAugmentation.lean, line 73	Every letter monomial maps to zero, for any coefficient.
MonoidAlgebra.freeMonoidAugmentation_apply	theorem	ProjectiveModules/Free/FreeWordAugmentation.lean, line 79	The zero-generator augmentation returns x.coeff 1, the coefficient of the empty word, for every free-word polynomial over any semiring. Noncommutative and trivial coefficients and empty or infinite alphabets are included, with independent coefficient and alphabet universes.
MonoidAlgebra.range_linearCombination_freeMonoid_of_eq_ker_freeMonoidAugmentation	theorem	ProjectiveModules/Free/FreeWordAugmentationKernel.lean, line 92	The range of Finsupp.linearCombination A of all letter monomials equals LinearMap.ker of the zero-generator augmentation's toSemilinearMap, with A = MonoidAlgebra K (FreeMonoid alphabet). Coordinates are A-valued and letters multiply on the right under the canonical left regular A-action. Only Semiring K is required; coefficient and alphabet universes are independent, including noncommutative or trivial coefficients and empty or infinite alphabets. No global Module A K instance, basis or linear equivalence onto the kernel is constructed.
Module.exists_fin_prod_linearEquiv_iff_finite_isStablyFree	theorem	ProjectiveModules/Free/StablePresentation.lean, line 51	Over arbitrary rings, existence of a finite-coordinate stable presentation is equivalent to finite generation and stable freeness, without IBN or a nontriviality assumption.
Module.card_add_card_eq_of_prod_linearEquiv	theorem	ProjectiveModules/Free/StablePresentation.lean, line 82	IBN-only cross-sum equality for any two finite-index presentations over semirings, with independent index universes and no freeness premise on the presented module.
Module.int_card_sub_eq_of_prod_linearEquiv	theorem	ProjectiveModules/Free/StablePresentation.lean, line 106	The associated integer coordinate differences agree without a rank condition, nonnegativity or natural subtraction.
Module.IsStablyFree.ker_of_surjective	theorem	ProjectiveModules/Free/StableKernel.lean, line 55	Over an arbitrary ring, a surjection from a stably-free module onto a finitely generated stably-free module has stably-free kernel. No finite generation of the domain is assumed or of the kernel is concluded.
Module.finite_isStablyFree_iff_exists_fin_surjective_ker_equiv	theorem	ProjectiveModules/Free/StableKernel.lean, line 96	Over an arbitrary ring, a module is finitely generated and stably free iff it is linearly equivalent to the kernel of a surjection between Fin n and Fin m coordinate modules for some natural m and n. This asserts neither a rank inequality nor an ordinary finite-presentation equivalence.
Matrix.finite_isStablyFree_ker_mulVecBilin_of_surjective	theorem	ProjectiveModules/Free/StableKernel.lean, line 156	For independently universe-polymorphic finite row and column index types over any ring, a surjective Matrix.mulVecBilin R Rᵐᵒᵖ A has finitely generated stably-free right-module kernel. Entries multiply coordinates on the left as A i j * x j. Empty index types and zero rings are included where surjectivity holds; no IBN, commutativity or free-kernel claim.
mk_eq_mk_of_basis_of_infinite	theorem	ProjectiveModules/Free/InfiniteCoordinates.lean, line 48	Equal lifted index cardinalities for two bases of the same module, when the first index is infinite over a nontrivial semiring; no IBN, SRC or commutativity.
Module.Basis.indexEquivOfInfinite	def	ProjectiveModules/Free/InfiniteCoordinates.lean, line 61	A choice of index equivalence for these bases; it need not carry one basis vector to another.
Module.Basis.indexEquivOfInfinite_eq_indexEquiv	theorem	ProjectiveModules/Free/InfiniteCoordinates.lean, line 66	Under IBN, the chosen index equivalence agrees with Basis.indexEquiv.
Finsupp.nonempty_linearEquiv_iff_equiv	theorem	ProjectiveModules/Free/InfiniteCoordinates.lean, line 77	With an infinite first index, free coordinate modules are linearly equivalent iff their index types are equivalent, including across index universes.
Finsupp.nonempty_linearEquiv_iff_lift_mk_eq	theorem	ProjectiveModules/Free/InfiniteCoordinates.lean, line 88	Equivalent lifted-cardinality criterion for free coordinates in distinct index universes.
Finsupp.not_nonempty_linearEquiv_of_infinite_finite	theorem	ProjectiveModules/Free/InfiniteCoordinates.lean, line 96	No linear equivalence from infinite to finite free coordinates over a nontrivial semiring.
Module.free_of_finite_isStablyFree_of_isSemisimpleRing	theorem	ProjectiveModules/Free/Semisimple.lean, line 70	Finite stably-free modules over arbitrary semisimple rings are free; not all semisimple modules.
ModuleCat.FiniteProjective	abbrev	ProjectiveModules/Category/FiniteProjective.lean, line 46	Finite projective modules as a full additive subcategory with finite biproducts over arbitrary rings.
ModuleCat.finite_iff_of_equivalence	theorem	ProjectiveModules/Category/ModuleEquivalence.lean, line 100	A given ModuleCat.{vR} R ≌ ModuleCat.{vS} S preserves and reflects Module.Finite over arbitrary rings, with independent scalar universes uR, uS and carrier universes vR, vS.
ModuleCat.isFiniteProjective_of_equivalence	theorem	ProjectiveModules/Category/ModuleEquivalence.lean, line 125	A given ModuleCat.{vR} R ≌ ModuleCat.{max uS vS} S sends the canonical finite-projective object property to itself. The source carrier is unrestricted; Small is not a public premise.
ModuleCat.isFiniteProjective_iff_of_equivalence	theorem	ProjectiveModules/Category/ModuleEquivalence.lean, line 149	A given ModuleCat.{max uR vR} R ≌ ModuleCat.{max uS vS} S preserves and reflects the canonical finite-projective object property, with no linearity, commutativity or freeness assumption.
OrderIso.isCompactElement	theorem	ProjectiveModules/Order/CompactlyGenerated.lean, line 51	Order isomorphisms map compact elements to compact elements in arbitrary partial orders.
OrderIso.isCompactElement_iff	theorem	ProjectiveModules/Order/CompactlyGenerated.lean, line 66	Compact-element preservation and reflection at independent universes, without completeness or a top element.
ModuleCat.finiteProjectiveEssentiallySmall	instance	ProjectiveModules/Category/FiniteProjectiveSmallness.lean, line 56	For an arbitrary Ring R : Type u and independent carrier universe v, ModuleCat.FiniteProjective.{u,v} R is EssentiallySmall.{u}, derived from the finitely generated module category without an assumed Small premise. A smaller carrier universe need not represent every finite projective isomorphism class.
ModuleCat.FiniteProjective.repr	def	ProjectiveModules/Category/FiniteProjectiveSmallness.lean, line 122	Bundle Module.Finite.repr R P as a finite projective object with carrier in the ring universe, for any finitely generated projective module P in an independent universe over an arbitrary ring.
ModuleCat.FiniteProjective.reprEquiv	def	ProjectiveModules/Category/FiniteProjectiveSmallness.lean, line 135	The ring-universe representative is linearly equivalent to the original finite projective module by Mathlib's Module.Finite.reprEquiv; no carrier or scalar Small hypothesis is assumed.
ModuleCat.FiniteProjective.isoClass	def	ProjectiveModules/Category/FiniteProjectiveSmallness.lean, line 261	Send arbitrary finite projective inputs to the existing skeleton of ModuleCat.FiniteProjective.{u,u} R after taking a ring-universe representative. Applying this to Rᵐᵒᵖ gives right-module classes. This is not a K₀ group or a group-completion construction.
ModuleCat.FiniteProjective.isoClass_eq_iff	theorem	ProjectiveModules/Category/FiniteProjectiveSmallness.lean, line 269	Equality of classes in the same ring-universe reference skeleton is equivalent to Nonempty (P ≃ₗ[R] Q) for finite projective inputs whose carrier universes may differ, with no commutativity or nontriviality assumption on R.
KTheory.ProjectiveClass	def	ProjectiveModules/KTheory/K0.lean, line 123	Ring-universe additive commutative monoid of direct-sum isomorphism classes of finite projective right modules over an arbitrary ring, using the complete ring-universe reference category. Module generators accept arbitrary independent carrier universes without a Small premise.
KTheory.ProjectiveClass.of_eq_iff	theorem	ProjectiveModules/KTheory/K0.lean, line 147	Equality of module classes is exactly nonempty linear equivalence, including inputs in independent universes. Zero, product, representative and carrier-lift equations give the characteristic generator API.
KTheory.ProjectiveClass.lift	def	ProjectiveModules/KTheory/K0.lean, line 296	Isomorphism-invariant object functions preserving zero and binary direct sums descend to additive maps into any AddZero target, with reference/module evaluation, extensionality and uniqueness laws.
KTheory.K0	abbrev	ProjectiveModules/KTheory/K0.lean, line 346	Mathlib's additive Grothendieck group of the projective class monoid, in the ring universe, for arbitrary rings including the zero ring. For arbitrary rings, generator equality means common stabilization, not necessarily module isomorphism.
KTheory.K0.lift	def	ProjectiveModules/KTheory/K0.lean, line 399	Additive class maps to any additive commutative group extend uniquely to K₀ homomorphisms. Restriction is inverse to extension, and module generator evaluation and homomorphism extensionality are provided.
KTheory.ProjectiveClass.map	def	ProjectiveModules/KTheory/ScalarExtension.lean, line 106	Scalar extension along an arbitrary unital ring homomorphism induces an additive map on finite-projective right-module classes. Evaluation accepts independent carrier universes; identity and composition agree as whole homomorphisms, including noncommutative and zero rings.
KTheory.K0.map	def	ProjectiveModules/KTheory/ScalarExtension.lean, line 220	The induced K₀ map extends the class map through group completion, agrees on every class and arbitrary-carrier module generator, and respects identity and composition as whole homomorphisms. This general-ring scalar-extension API alone asserts no injectivity, dimension classification or cancellation of projective modules.
KTheory.ProjectiveClass.map_eq_map	theorem	ProjectiveModules/KTheory/ScalarExtension.lean, line 193	Any two unital homomorphisms from a fixed division ring to a fixed ring induce equal whole additive class maps. A finite source basis compares both extensions with the same target coordinate module; the target may be noncommutative or a zero ring, without a target dimension invariant.
KTheory.K0.map_eq_map	theorem	ProjectiveModules/KTheory/ScalarExtension.lean, line 330	The whole K₀ homomorphisms induced by two maps from a division ring to an arbitrary ring agree, by the class equality and group-completion extensionality. No injectivity of the class-to-K₀ map is assumed.
KTheory.K0.exists_sub	theorem	ProjectiveModules/KTheory/Stabilization.lean, line 86	Every K₀ element is a difference of two finite projective right-module generators in the complete ring-universe reference category. The chosen representative pair has a reconstruction law, not uniqueness or additivity.
KTheory.K0.of_eq_iff_exists_projective_stabilizer	theorem	ProjectiveModules/KTheory/Stabilization.lean, line 95	Two finite projective generators agree exactly when their modules become linearly equivalent after adjoining one common finite projective module in the ring universe. No module cancellation or nonzero-ring premise.
KTheory.K0.of_eq_iff_exists_free_stabilizer	theorem	ProjectiveModules/KTheory/Stabilization.lean, line 123	Generator equality is equivalent to linear equivalence after adjoining the same Fin n → Rᵐᵒᵖ. The rank n is existential, without IBN or a prescribed rank; input carrier universes may differ.
KTheory.K0.sub_eq_sub_iff_exists_projective_stabilizer	theorem	ProjectiveModules/KTheory/Stabilization.lean, line 145	Equality [P] - [Q] = [P'] - [Q'] is equivalent to linear equivalence of the cross-sums P × Q' and P' × Q after one common finite projective stabilizer. All four input carrier universes are independent.
KTheory.K0.sub_eq_sub_iff_exists_free_stabilizer	theorem	ProjectiveModules/KTheory/Stabilization.lean, line 165	The same difference equality is equivalent to stabilization of its cross-sums by one common standard finite free module. Cancellation is in the abelian group only, not among projective modules.
KTheory.ProjectiveClass.finrankHom	def	ProjectiveModules/KTheory/Rank.lean, line 97	Finite dimension descends to a natural-valued additive class map over a division ring. Evaluation requires finite generation, with freeness and projectivity supplied by division-ring scalars. This is the whole forward homomorphism of ProjectiveClass.finrankEquiv.
KTheory.ProjectiveClass.finrankEquiv	def	ProjectiveModules/KTheory/Rank.lean, line 161	For DivisionRing D, an AddEquiv ProjectiveClass D ≃+ ℕ whose forward homomorphism is the canonical finrankHom. Its inverse sends every n to the class of Fin n → Dᵐᵒᵖ. Both canonical-map round trips, arbitrary-carrier finite-module evaluation and dimension recovery, and regular-class one and inverse-one laws are provided.
KTheory.K0.finrankHom	def	ProjectiveModules/KTheory/Rank.lean, line 233	Integer-valued K₀ dimension uniquely extends natural class dimension, evaluates on finitely generated modules in arbitrary carrier universes, and sends the regular generator to one. This is the whole forward homomorphism of K0.finrankEquiv.
KTheory.K0.finrankEquiv	def	ProjectiveModules/KTheory/Rank.lean, line 325	For DivisionRing D, an AddEquiv K0 D ≃+ ℤ whose forward homomorphism is the canonical finrankHom. Its inverse sends every integer z, including negatives, to z • K0.of D Dᵐᵒᵖ; natural casts recover finite-coordinate generators. Both canonical-map round trips, arbitrary-carrier finite-module evaluation and dimension recovery, regular-generator one and inverse-one laws, and class-completion compatibility are provided. Equality of finite-module generators is equivalent to right-linear isomorphism over division rings only.

Quoted from the main results in formalization.yaml of FormalFrontier/projective-modules at commit 27f95a8b, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.