Equiv

📁 Source: Mathlib/Algebra/Order/Module/Equiv.lean

Statistics

Metric	Count
Definitions ofLexLinearEquiv, toLexLinearEquiv	2
Theorems coe_ofLexLinearEquiv, coe_toLexLinearEquiv, symm_ofLexLinearEquiv, symm_toLexLinearEquiv	4
Total	6

(root)

Definitions

Name	Category	Theorems
ofLexLinearEquiv 📖	CompOp	3 math math: symm_toLexLinearEquiv, coe_ofLexLinearEquiv, symm_ofLexLinearEquiv
toLexLinearEquiv 📖	CompOp	3 math math: symm_toLexLinearEquiv, coe_toLexLinearEquiv, symm_ofLexLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofLexLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Lex instAddCommMonoidLex Lex.instModule' EquivLike.toFunLike LinearEquiv.instEquivLike ofLexLinearEquiv Equiv Equiv.instEquivLike ofLex	—	RingHomInvPair.ids
coe_toLexLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Lex instAddCommMonoidLex Lex.instModule' EquivLike.toFunLike LinearEquiv.instEquivLike toLexLinearEquiv Equiv Equiv.instEquivLike toLex	—	RingHomInvPair.ids
symm_ofLexLinearEquiv 📖	mathematical	—	LinearEquiv.symm Lex instAddCommMonoidLex Lex.instModule' RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ofLexLinearEquiv toLexLinearEquiv	—	RingHomInvPair.ids
symm_toLexLinearEquiv 📖	mathematical	—	LinearEquiv.symm Lex instAddCommMonoidLex Lex.instModule' RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids toLexLinearEquiv ofLexLinearEquiv	—	RingHomInvPair.ids

---

← Back to Index