div

Mathlib.Geometry.Manifold.Algebra.LieGroup

URI: https://scilib.ai/kg/mathlib#ContMDiff.div

← MathLib Explorer

English

If f and g are ContMDiff on a domain, then f/g is ContMDiff on that domain.

Русский

Если f и g гладкие, то f/g гладко на своей области.

LaTeX

$$ContMDiff I n f → ContMDiff I n g → ContMDiff I n (fun x => f x / g x)$$

Lean4

@[to_additive]
theorem div {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n fun x => f x / g x :=
  by simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru