MulOpposite

📁 Source: Mathlib/LinearAlgebra/Basis/MulOpposite.lean

Statistics

Metric	Count
Definitions mulOpposite	1
Theorems mulOpposite_apply, mulOpposite_repr_eq, mulOpposite_repr_op, repr_unop_eq_mulOpposite_repr, finrank, instFiniteDimensional, instFree, rank	8
Total	9

Module.Basis

Definitions

Name	Category	Theorems
mulOpposite 📖	CompOp	6 math math: mulOpposite_apply, mulOpposite_is_orthonormal_iff, OrthonormalBasis.toBasis_mulOpposite, mulOpposite_repr_op, mulOpposite_repr_eq, repr_unop_eq_mulOpposite_repr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulOpposite_apply 📖	mathematical	—	DFunLike.coe Module.Basis MulOpposite MulOpposite.instAddCommMonoid MulOpposite.instModule instFunLike mulOpposite MulOpposite.op	—	—
mulOpposite_repr_eq 📖	mathematical	—	repr MulOpposite MulOpposite.instAddCommMonoid MulOpposite.instModule mulOpposite LinearEquiv.trans Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv	—	RingHomInvPair.ids
mulOpposite_repr_op 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOpposite Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring MulOpposite.instAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid MulOpposite.instModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr mulOpposite MulOpposite.op	—	RingHomInvPair.ids
repr_unop_eq_mulOpposite_repr 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr MulOpposite.unop MulOpposite MulOpposite.instAddCommMonoid MulOpposite.instModule mulOpposite	—	RingHomInvPair.ids

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank 📖	mathematical	—	Module.finrank MulOpposite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring instAddCommMonoid AddCommGroup.toAddCommMonoid instModule	—	Module.finrank_eq_nat_card_basis IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing
instFiniteDimensional 📖	mathematical	—	FiniteDimensional MulOpposite instAddCommGroup instModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	FiniteDimensional.of_finite_basis Set.toFinite Finite.of_fintype
instFree 📖	mathematical	—	Module.Free MulOpposite instAddCommMonoid instModule	—	Module.Free.exists_basis Module.Free.of_basis
rank 📖	mathematical	—	Module.rank MulOpposite instAddCommMonoid instModule	—	RingHomInvPair.ids LinearEquiv.nonempty_equiv_iff_rank_eq instFree

---

← Back to Index