Inverse

📁 Source: Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Statistics

Metric	Count
Definitions instInv, instInvOneClass, inv, aux, invOfUnit	5
Theorems C_inv, X_inv, coeff_inv, coeff_invOfUnit, coeff_inv_aux, constantCoeff_inv, constantCoeff_invOfUnit, eq_inv_iff_mul_eq_one, eq_mul_inv_iff_mul_eq, instIsLocalRing, invOfUnit_eq, invOfUnit_eq', invOfUnit_mul, inv_eq_iff_mul_eq_one, inv_eq_zero, inv_mul_cancel, isUnit_iff_constantCoeff, isLocalHom, mul_invOfUnit, mul_inv_cancel, mul_inv_rev, smul_inv, zero_inv	23
Total	28

MvPowerSeries

Definitions

Name	Category	Theorems
instInv 📖	CompOp	32 math math: zero_inv, PowerSeries.derivative_inv', PowerSeries.inv_eq_iff_mul_eq_one, PowerSeries.eq_mul_inv_iff_mul_eq, eq_inv_iff_mul_eq_one, inv_eq_iff_mul_eq_one, constantCoeff_inv, coeff_inv, inv_mul_cancel, PowerSeries.X_inv, C_inv, PowerSeries.constantCoeff_inv, PowerSeries.mul_inv_cancel, PowerSeries.mul_inv_rev, PowerSeries.invOfUnit_eq', PowerSeries.zero_inv, PowerSeries.inv_eq_zero, PowerSeries.invOfUnit_eq, inv_eq_zero, PowerSeries.coeff_inv, PowerSeries.eq_inv_iff_mul_eq_one, X_inv, mul_inv_cancel, PowerSeries.C_inv, invOfUnit_eq', eq_mul_inv_iff_mul_eq, PowerSeries.inv_eq_inv_aux, invOfUnit_eq, mul_inv_rev, PowerSeries.smul_inv, smul_inv, PowerSeries.inv_mul_cancel
instInvOneClass 📖	CompOp	—
inv 📖	CompOp	—
invOfUnit 📖	CompOp	6 math math: constantCoeff_invOfUnit, invOfUnit_mul, coeff_invOfUnit, mul_invOfUnit, invOfUnit_eq', invOfUnit_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_inv 📖	mathematical	—	MvPowerSeries instInv DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instSemiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_inv inv_zero inv_eq_iff_mul_eq_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass inv_mul_cancel₀ map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
X_inv 📖	mathematical	—	MvPowerSeries instInv X DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	inv_eq_zero constantCoeff_X
coeff_inv 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff instInv Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero Finsupp.instDecidableEq InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero RingHom instSemiring RingHom.instFunLike constantCoeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Finset.sum Finset.HasAntidiagonal.antidiagonal Finsupp.instAddMonoid Nat.instAddMonoid Finsupp.instHasAntidiagonal Preorder.toLT Finsupp.preorder Nat.instPreorder Finsupp.decidableLT Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd NonUnitalNonAssocSemiring.toMulZeroClass	—	coeff_inv_aux
coeff_invOfUnit 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff invOfUnit Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero Finsupp.instDecidableEq Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Units.instInv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Finset.sum Finset.HasAntidiagonal.antidiagonal Finsupp.instAddMonoid Nat.instAddMonoid Finsupp.instHasAntidiagonal Preorder.toLT Finsupp.preorder Nat.instPreorder Finsupp.decidableLT Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd Finset.sum_congr coeff_inv_aux
coeff_inv_aux 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff inv.aux Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero Finsupp.instDecidableEq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Finset.sum Finset.HasAntidiagonal.antidiagonal Finsupp.instAddMonoid Nat.instAddMonoid Finsupp.instHasAntidiagonal Preorder.toLT Finsupp.preorder Nat.instPreorder Finsupp.decidableLT Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd inv.aux.eq_1
constantCoeff_inv 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike constantCoeff instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	coeff_zero_eq_constantCoeff_apply Nat.instCanonicallyOrderedAdd coeff_inv
constantCoeff_invOfUnit 📖	mathematical	—	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring Ring.toSemiring RingHom.instFunLike constantCoeff invOfUnit Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Units.instInv	—	coeff_zero_eq_constantCoeff_apply Nat.instCanonicallyOrderedAdd coeff_invOfUnit
eq_inv_iff_mul_eq_one 📖	mathematical	—	MvPowerSeries instInv instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instOne	—	eq_mul_inv_iff_mul_eq one_mul
eq_mul_inv_iff_mul_eq 📖	mathematical	—	MvPowerSeries instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instInv	—	mul_assoc inv_mul_cancel mul_one mul_inv_cancel
instIsLocalRing 📖	mathematical	—	IsLocalRing MvPowerSeries instSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsLocalRing.of_isUnit_or_isUnit_one_sub_self instNontrivial IsLocalRing.toNontrivial IsLocalRing.isUnit_or_isUnit_one_sub_self IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid mul_invOfUnit map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
invOfUnit_eq 📖	mathematical	—	invOfUnit DivisionRing.toRing Field.toDivisionRing DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring DivisionSemiring.toSemiring RingHom.instFunLike constantCoeff instInv	—	—
invOfUnit_eq' 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike constantCoeff Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	invOfUnit DivisionRing.toRing Field.toDivisionRing MvPowerSeries instInv	—	Units.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing invOfUnit_eq Units.ext_iff
invOfUnit_mul 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring Ring.toSemiring RingHom.instFunLike constantCoeff Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	MvPowerSeries instMul Ring.toSemiring invOfUnit instOne	—	mul_cancel_right_mem_nonZeroDivisors mem_nonZeroDivisors_of_constantCoeff constantCoeff_invOfUnit IsUnit.mem_nonZeroDivisors Units.isUnit mul_assoc one_mul mul_invOfUnit mul_one
inv_eq_iff_mul_eq_one 📖	mathematical	—	MvPowerSeries instInv instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instOne	—	eq_inv_iff_mul_eq_one
inv_eq_zero 📖	mathematical	—	MvPowerSeries instInv instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike constantCoeff	—	constantCoeff_inv ext Nat.instCanonicallyOrderedAdd coeff_inv inv_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_zero MulZeroClass.zero_mul
inv_mul_cancel 📖	mathematical	—	MvPowerSeries instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instInv instOne	—	mul_comm mul_inv_cancel
isUnit_iff_constantCoeff 📖	mathematical	—	IsUnit MvPowerSeries MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Ring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike constantCoeff	—	IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_invOfUnit invOfUnit_mul
mul_invOfUnit 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring Ring.toSemiring RingHom.instFunLike constantCoeff Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	MvPowerSeries instMul Ring.toSemiring invOfUnit instOne	—	ext map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass constantCoeff_invOfUnit Units.mul_inv Finset.HasAntidiagonal.mem_antidiagonal zero_add coeff_one coeff_mul Finset.insert_erase Finset.sum_insert Finset.notMem_erase coeff_zero_eq_constantCoeff_apply Nat.instCanonicallyOrderedAdd coeff_invOfUnit neg_mul mul_neg Units.mul_inv_cancel_left not_lt_of_ge le_rfl add_comm sub_eq_add_neg sub_eq_zero Finset.sum_congr Finset.mem_erase lt_add_of_pos_left IsRightCancelAdd.addRightStrictMono_of_addRightMono Finsupp.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finsupp.isOrderedAddMonoid pos_iff_ne_zero Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub
mul_inv_cancel 📖	mathematical	—	MvPowerSeries instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instInv instOne	—	invOfUnit_eq mul_invOfUnit
mul_inv_rev 📖	mathematical	—	MvPowerSeries instInv instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	inv_eq_zero map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IsDomain.to_noZeroDivisors Field.isDomain MulZeroClass.mul_zero MulZeroClass.zero_mul inv_eq_iff_mul_eq_one mul_assoc inv_mul_cancel mul_one
smul_inv 📖	mathematical	—	MvPowerSeries instInv Algebra.toSMul Semifield.toCommSemiring Field.toSemifield instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebra Algebra.id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	smul_eq_C_mul mul_comm mul_inv_rev C_inv
zero_inv 📖	mathematical	—	MvPowerSeries instInv instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	inv_eq_zero constantCoeff_zero

MvPowerSeries.inv

Definitions

Name	Category	Theorems
aux 📖	CompOp	1 math math: MvPowerSeries.coeff_inv_aux

MvPowerSeries.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalHom 📖	mathematical	—	IsLocalHom MvPowerSeries RingHom Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike MvPowerSeries.map	—	MvPowerSeries.isUnit_constantCoeff Units.isUnit isUnit_of_map_unit MvPowerSeries.constantCoeff_map IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid MvPowerSeries.mul_invOfUnit

---

← Back to Index