Theorems · Definition · commutative algebra
AddMonoidAlgebra.divOf
{k : Type u_1} →
{G : Type u_2} →
[inst : Semiring k] → [inst_1 : AddCommMonoid G] → [IsCancelAdd G] → AddMonoidAlgebra k G → G → AddMonoidAlgebra k GDivide by of' k G g, discarding terms not divisible by this.
- Defined in
- Mathlib.Algebra.MonoidAlgebra.Division
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- AddMonoidAlgebrastatement and proof · cited by 649
- AddMonoidAlgebra.coeffproof · cited by 365
- IsCancelAddstatement and proof · cited by 79
- Finsupp.comapDomainproof · cited by 40
Cited by20
Results whose statement or proof uses this declaration.
- Polynomial.divXproof · cited by 25
- MvPolynomial.divMonomialproof · cited by 21
- AddMonoidAlgebra.divOf_add_modOfstatement and proof · cited by 3
- AddMonoidAlgebra.mul_of'_divOfstatement · cited by 2
- AddMonoidAlgebra.coeff_divOfstatement · cited by 2
- AddMonoidAlgebra.modOf_add_divOfstatement and proof · cited by 1
- AddMonoidAlgebra.add_divOfstatement · cited by 1
- AddMonoidAlgebra.divOf.congr_simpstatement and proof · cited by 1
- AddMonoidAlgebra.divOfHomproof · cited by 1
- AddMonoidAlgebra.divOf_addstatement · cited by 1
- AddMonoidAlgebra.divOf_zerostatement · cited by 1
- AddMonoidAlgebra.of'_divOfstatement · cited by 1