Basic

📁 Source: Mathlib/LinearAlgebra/Projectivization/Basic.lean

Statistics

Metric	Count
Definitions termℙ, Projectivization, equivSubmodule, map, mk, mk', mk'', rep, submodule, projectivizationSetoid	10
Theorems exists_smul_eq_mk_rep, finrank_submodule, ind, instFiniteDimensionalSubtypeMemSubmoduleSubmodule, instNonemptyOfNontrivial, lift_mk, map_comp, map_id, map_injective, map_mk, mk''_submodule, mk'_eq_mk, mk_eq_mk_iff, mk_eq_mk_iff', mk_rep, rep_nonzero, submodule_eq, submodule_injective, submodule_mk, submodule_mk''	20
Total	30

LinearAlgebra.Projectivization

Definitions

Name	Category	Theorems
termℙ 📖	CompOp	—

Projectivization

Definitions

Name	Category	Theorems
equivSubmodule 📖	CompOp	—
map 📖	CompOp	6 math math: map_id, map_injective, smul_def, map_comp, generalLinearGroup_smul_def, map_mk
mk 📖	CompOp	—
mk' 📖	CompOp	1 math math: mk'_eq_mk
mk'' 📖	CompOp	2 math math: submodule_mk'', mk''_submodule
rep 📖	CompOp	5 math math: submodule_eq, mk_rep, exists_smul_eq_mk_rep, dependent_iff, independent_iff
submodule 📖	CompOp	9 math math: submodule_mk'', submodule_eq, finrank_submodule, submodule_mk, independent_iff_iSupIndep, submodule_injective, Submodule.mem_projectivization_iff_submodule_le, instFiniteDimensionalSubtypeMemSubmoduleSubmodule, mk''_submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_eq_mk_rep 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid rep	—	rep_nonzero mk_eq_mk_iff mk_rep
finrank_submodule 📖	mathematical	—	Module.finrank Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike submodule Submodule.addCommMonoid Submodule.module	—	submodule_eq finrank_span_singleton rep_nonzero
ind 📖	—	—	—	—	Quotient.ind'
instFiniteDimensionalSubtypeMemSubmoduleSubmodule 📖	mathematical	—	FiniteDimensional Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike submodule Submodule.addCommGroup DivisionRing.toRing Submodule.module	—	rep_nonzero mk_rep FiniteDimensional.span_singleton
instNonemptyOfNontrivial 📖	mathematical	—	Projectivization	—	exists_ne
lift_mk 📖	mathematical	—	lift NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
map_comp 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.comp	map Projectivization	—	—
map_id 📖	mathematical	—	map RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring LinearMap.id AddCommGroup.toAddCommMonoid LinearEquiv.injective RingHomInvPair.ids LinearEquiv.refl Projectivization	—	LinearEquiv.injective RingHomInvPair.ids
map_injective 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	Projectivization map	—	ind map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_smulₛₗ RingHomInvPair.comp_apply_eq₂
map_mk 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	map AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass	—	—
mk''_submodule 📖	mathematical	—	mk'' submodule finrank_submodule	—	Equiv.symm_apply_apply
mk'_eq_mk 📖	mathematical	—	mk' NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
mk_eq_mk_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Quotient.eq''
mk_eq_mk_iff' 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	mk_eq_mk_iff zero_smul
mk_rep 📖	mathematical	—	rep rep_nonzero	—	Quotient.out_eq'
rep_nonzero 📖	—	—	—	—	—
submodule_eq 📖	mathematical	—	submodule Submodule.span DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instSingletonSet rep	—	rep_nonzero mk_rep
submodule_injective 📖	mathematical	—	Projectivization Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid submodule	—	ind mk_eq_mk_iff Submodule.span_singleton_eq_span_singleton DivisionRing.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
submodule_mk 📖	mathematical	—	submodule Submodule.span DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instSingletonSet	—	—
submodule_mk'' 📖	mathematical	Module.finrank Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	submodule mk''	—	Equiv.apply_symm_apply

(root)

Definitions

Name	Category	Theorems
Projectivization 📖	CompOp	45 math math: Projectivization.dependent_pair_iff_eq, Projectivization.map_id, Projectivization.Subspace.span_sup, Projectivization.card'', Projectivization.Subspace.span_empty, Projectivization.Subspace.span_coe, Submodule.mk_mem_projectivization_iff, Projectivization.finite_of_finite, Projectivization.isEmpty_of_subsingleton, Projectivization.finite_iff_of_finite, Projectivization.submodule_injective, Projectivization.card, Configuration.ofField.instNondegenerateProjectivizationForallFinOfNatNat, OnePoint.equivProjectivization_symm_apply_mk, Projectivization.Subspace.subset_span, Projectivization.independent_pair_iff_ne, Projectivization.map_injective, Submodule.mem_projectivization_iff_submodule_le, Projectivization.card_of_finrank, Projectivization.Subspace.sup_span, Projectivization.Subspace.monotone_span, Projectivization.cross_mk, Projectivization.dependent_iff, Projectivization.card', Projectivization.Subspace.span_le_subspace_iff, Projectivization.smul_def, Projectivization.map_comp, OnePoint.smul_infty_def, Projectivization.Subspace.mem_span, Projectivization.cross_mk_of_ne, Projectivization.Subspace.span_union, Projectivization.generalLinearGroup_smul_def, Projectivization.Subspace.span_univ, Projectivization.card_of_finrank_two, OnePoint.equivProjectivization_apply_coe, Configuration.ofField.mem_iff, Projectivization.instNonemptyOfNontrivial, Projectivization.independent_iff, Projectivization.Subspace.span_eq_span_iff, Projectivization.Subspace.mem_carrier_iff, Projectivization.Subspace.span_eq_sInf, Projectivization.smul_mk, Projectivization.Subspace.span_iUnion, Projectivization.Subspace.mem_submodule_iff, OnePoint.equivProjectivization_apply_infinity
projectivizationSetoid 📖	CompOp	—

---

← Back to Index