Documentation Verification Report

Balance

📁 Source: Mathlib/Algebra/BigOperators/Balance.lean

Statistics

Metric	Count
Definitions `balance`	1
Theorems `balance_add`, `balance_apply`, `balance_idem`, `balance_neg`, `balance_sub`, `balance_zero`, `expect_balance`, `map_balance`, `sum_balance`	9
Total	10

Fintype

Definitions

Name	Category	Theorems
`balance` 📖	CompOp	17 math math: `balance_add`, `balance_zero`, `Complex.re_balance`, `RCLike.ofReal_balance`, `RCLike.ofReal_comp_balance`, `Complex.re_comp_balance`, `Complex.ofReal_balance`, `balance_apply`, `Complex.ofReal_comp_balance`, `Complex.im_balance`, `balance_neg`, `Complex.im_comp_balance`, `expect_balance`, `map_balance`, `balance_idem`, `sum_balance`, `balance_sub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`balance_add` 📖	mathematical	—	`balance` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Finset.expect_congr` `Finset.expect_add_distrib` `add_sub_add_comm`
`balance_apply` 📖	mathematical	—	`balance` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Finset.expect` `AddCommGroup.toAddCommMonoid` `Finset.univ`	—	—
`balance_idem` 📖	mathematical	—	`balance`	—	`isEmpty_or_nonempty` `Finset.expect_congr` `Finset.univ_eq_empty` `Finset.expect_empty` `sub_zero` `Finset.expect_sub_distrib` `Finset.expect_const` `sub_self`
`balance_neg` 📖	mathematical	—	`balance` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.expect_congr` `Finset.expect_neg_distrib` `neg_sub'`
`balance_sub` 📖	mathematical	—	`balance` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Finset.expect_congr` `Finset.expect_sub_distrib` `sub_sub_sub_comm`
`balance_zero` 📖	mathematical	—	`balance` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.expect_congr` `Finset.expect_const_zero` `sub_self`
`expect_balance` 📖	mathematical	—	`Finset.expect` `AddCommGroup.toAddCommMonoid` `Finset.univ` `balance` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.sum_congr` `sum_balance` `smul_zero`
`map_balance` 📖	mathematical	—	`DFunLike.coe` `balance`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `map_expect` `Finset.expect_congr`
`sum_balance` 📖	mathematical	—	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `balance` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`isEmpty_or_nonempty` `Finset.sum_congr` `Finset.univ_eq_empty` `Finset.expect_congr` `Finset.expect_empty` `sub_zero` `Finset.sum_sub_distrib` `Finset.sum_const` `card_smul_expect` `sub_self`

---

← Back to Index