inf rule name 
inputs 
outputs 
feeds 
Latex 
Used in derivations 
number of uses 
assumptions 
LHS of expr 1 equals LHS of expr 2 
2 
1 
0 
LHS of Eq.~ref{eq:#1} is equal to LHS of Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

16


RHS of expr 1 equals RHS of expr 2 
2 
1 
0 
RHS of Eq.~ref{eq:#1} is equal to RHS of Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

1


X cross both sides by 
1 
1 
1 
Take cross product of $#1$ and Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

0

linear algebra 
X dot both sides 
1 
1 
1 
Take inner product of $#1$ with Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

0

linear algebra 
add X to both sides 
1 
1 
1 
Add $#1$ to both sides of Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

15


add expr 1 to expr 2 
2 
1 
0 
Add Eq.~ref{eq:#1} to Eq.~ref{eq:#2}; yields Eq.~ref{eq:#2}. 

3


add zero to LHS 
1 
1 
1 
Add zero to LHS of Eq.~ref{eq:#2}, where $0=#1$; yields Eq.~ref{eq:#3}. 

0


add zero to RHS 
1 
1 
1 
Add zero to RHS of Eq.~ref{eq:#2}, where $0=#1$; yields Eq.~ref{eq:#3}. 

0


apply divergence 
1 
1 
0 
Apply divergence to both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

multivariable calculus 
apply function to both sides of expression 
1 
1 
2 
Apply function $#1$ with argument $#2$ to Eq.~ref{eq:#3}; yields Eq.~ref{eq:#4} 

1


apply gradient to scalar function 
1 
1 
0 
Apply gradient to both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

multivariable calculus 
apply operator to bra 
1 
1 
0 
Apply operator in Eq.~ref{eq:#1} to bra; yields Eq.~ref{eq:#2}. 

1

quantum: Dirac notation 
apply operator to ket 
1 
1 
0 
Apply operator in Eq.~ref{eq:#1} to ket; yields Eq.~ref{eq:#2}. 

1

quantum: Dirac notation 
assume N dimensions 
0 
1 
1 
Assume $#1$ dimensions; decompose vector to be Eq.~ref{eq:#2}. 

3


both sides cross X 
1 
1 
1 
Take cross product of Eq.~ref{eq:#2} and $#1$; yields Eq.~ref{eq:#3} 

0

linear algebra 
both sides dot X 
1 
1 
1 
Take inner product of Eq.~ref{eq:#2} with $#1$; yields Eq.~ref{eq:#3} 

0

linear algebra 
boundary condition 
1 
1 
0 
Boundary condition: Eq.~ref{eq:#2} when Eq.~ref{eq#1}. 

2


boundary condition for expr 
1 
1 
0 
A boundary condition for Eq.~ref{eq:#1} is Eq.~ref{eq:#2} 

2


change five variables in expr 
1 
1 
10 
Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ and $#9$ to $#10$ in Eq.~ref{eq:#11}; yields Eq.~ref{eq:#12}. 

0


change four variables in expr 
1 
1 
8 
Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ in Eq.~ref{eq:#9}; yields Eq.~ref{eq:#10}. 

2


change six variables in expr 
1 
1 
12 
Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ and $#9$ to $#10$ and $#11$ to $#12$ in Eq.~ref{eq:#13}; yields Eq.~ref{eq:#14}. 

0


change three variables in expr 
1 
1 
6 
Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ in Eq.~ref{eq:#7}; yields Eq.~ref{eq:#8}. 

7


change two variables in expr 
1 
1 
4 
Change variable $#1$ to $#2$ and $#3$ to $#4$ in Eq.~ref{eq:#5}; yields Eq.~ref{eq:#6}. 

21


change variable X to Y 
1 
1 
2 
Change variable $#1$ to $#2$ in Eq.~ref{eq:#3}; yields Eq.~ref{eq:#4}. 

24


claim LHS equals RHS 
1 
0 
0 
Thus we see that LHS of Eq.~ref{eq:#1} is equal to RHS. 

3


claim expr 1 equals expr 2 
2 
0 
0 
Thus we see that Eq.~ref{eq:#1} is equivalent to Eq.~ref{eq:#2}. 

0


combine like terms 
1 
1 
0 
Combine like terms in Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1


conjugate both sides 
1 
1 
0 
Conjugate both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

3

complex values 
conjugate function X 
1 
1 
1 
Conjugate $#1$ in Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

1

complex values 
conjugate transpose both sides 
1 
1 
0 
Conjugate transpose of both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

complex valued linear algebra 
declare assumption 
0 
1 
0 
Eq.~ref{eq:#1} is an assumption. 

14


declare final expr 
1 
0 
0 
Eq.~ref{eq:#1} is one of the final equations. 

42


declare guess solution 
1 
1 
0 
Judicious choice as a guessed solution to Eq.~ref{eq:#1} is Eq.~ref{eq:#2}, 

3


declare identity 
0 
1 
0 
Eq.~ref{eq:#1} is an identity. 

12


declare initial expr 
0 
1 
0 
Eq.~ref{eq:#1} is an initial equation. 

113


differentiate with respect to 
1 
1 
1 
Differentiate Eq.~ref{eq:#2} with respect to $#1$; yields Eq.~ref{eq:#3}. 

5

differential equations 
distribute conjugate to factors 
1 
1 
0 
Distribute conjugate to factors in Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

complex values 
distribute conjugate transpose to factors 
1 
1 
0 
Distribute conjugate transpose to factors in Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

complex valued linear algebra 
divide both sides by 
1 
1 
1 
Divide both sides of Eq.~ref{eq:#2} by $#1$; yields Eq.~ref{eq:#3}. 

37


divide expr 1 by expr 2 
2 
1 
0 
Divide Eq.~ref{eq:#1} by Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

1


drop nondominant term 
1 
1 
1 
Based on the assumption $#1$, drop nondominant term in Eq.~ref{#2}; yeilds Eq.~ref{#3} 

2


evaluate definite integral 
1 
1 
0 
Evaluate definite integral Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

3

multivariable calculus 
expand LHS 
1 
1 
0 
Expand the LHS of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

0


expand RHS 
1 
1 
0 
Expand the RHS of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1


expand integrand 
1 
1 
0 
Expand integrand of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

multivariable calculus 
expand magnitude to conjugate 
1 
1 
1 
Expand $#1$ in Eq.~ref{eq:#2} with conjugate; yields Eq.~ref{eq:#3}. 

1

complex values 
expr 1 is equivalent to expr 2 under the condition 
2 
1 
0 
Eq.~ref{eq:#1} is equivalent to Eq.~ref{eq:#2} under the condition in Eq.~ref{eq:#3}. 

3


expr 1 is true under condition expr 2 
2 
1 
0 
Eq.~ref{eq:#1} is valid when Eq.~ref{eq:#2} occurs; yields Eq.~ref{eq:#3}. 

1


factor out X 
1 
1 
1 
Factor $#1$ from Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

0


factor out X from LHS 
1 
1 
1 
Factor $#1$ from the LHS of Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

2


factor out X from RHS 
1 
1 
1 
Factor $#1$ from the RHS of Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

1


function is even 
1 
1 
3 
$#1$ is even with respect to $#2$, so replace $#1$ with $#3$ in Eq.~ref{eq:#4}; yields Eq.~ref{eq:#5}. 

1


function is odd 
1 
1 
3 
$#1$ is odd with respect to $#2$, so replace $#1$ with $#3$ in Eq.~ref{eq:#4}; yields Eq.~ref{eq:#5}. 

1


indefinite integral over 
1 
1 
1 
Indefinite integral of both sides of Eq.~ref{eq:#2} over $#1$; yields Eq.~ref{eq:#3}. 

0

multivariable calculus 
indefinite integrate LHS over 
1 
1 
1 
Indefinite integral of LHS of Eq.~ref{eq:#2} over $#1$; yields Eq.~ref{eq:#3}. 

0

multivariable calculus 
indefinite integrate RHS over 
1 
1 
1 
Indefinite integral of RHS of Eq.~ref{eq:#2} over $#1$; yields Eq.~ref{eq:#3}. 

2

multivariable calculus 
indefinite integration 
1 
1 
0 
Indefinite integral of both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

5

multivariable calculus 
integrate 
1 
1 
0 
Integrate Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

2

multivariable calculus 
integrate over from to 
1 
1 
3 
Integrate Eq.~ref{eq:#4} over $#1$ from lower limit $#2$ to upper limit $#3$; yields Eq.~ref{eq:#5}. 

0

multivariable calculus 
make expr power 
1 
1 
1 
Make Eq.~ref{eq:#2} the power of $#1$; yields Eq.~ref{eq:#3}. 

1


maximum of expr 
1 
1 
1 
The maximum of Eq.~ref{eq:#2} with respect to $#1$ is Eq.~ref{eq:#3} 

2


multiply LHS by unity 
1 
1 
1 
Multiply LHS of Eq.~ref{eq:#2} by 1, which in this case is $#1$; yields Eq.~ref{eq:#3} 

0


multiply RHS by unity 
1 
1 
1 
Multiply RHS of Eq.~ref{eq:#2} by 1, which in this case is $#1$; yields Eq.~ref{eq:#3} 

2


multiply both sides by 
1 
1 
1 
Multiply both sides of Eq.~ref{eq:#2} by $#1$; yields Eq.~ref{eq:#3}. 

31


multiply expr 1 by expr 2 
2 
1 
0 
Multiply Eq.~ref{eq:#1} by Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

8


normalization condition 
0 
1 
0 
Normalization condition is Eq.~ref{eq:#1}. 

1


partially differentiate with respect to 
1 
1 
1 
Partially differentiate Eq.~ref{eq:#2} with respect to $#1$; yields Eq.~ref{eq:#3}. 

2

differential equations 
raise both sides to power 
1 
1 
1 
Raise both sides of Eq.~ref{eq:#2} to $#1$; yields Eq.~ref{eq:#3}. 

5


replace constant with value 
1 
1 
3 
Replace constant $#1$ with value $#2$ and units $#3$ in Eq.~ref{eq:#4}; yields Eq.~ref{eq:#5} 

3


replace curl with LeviCevita summation contravariant 
1 
1 
0 
Replace curl in Eq.~ref{eq:#1} with LeviCevita contravariant; yields Eq.~ref{eq:#2}. 

2

linear algebra 
replace scalar with vector 
1 
1 
0 
Replace scalar variables in Eq.~ref{eq:#1} with equivalent vector variables; yields Eq.~ref{eq:#2}. 

1


replace summation notation with vector notation 
1 
1 
0 
Replace summation notation in Eq.~ref{eq:#1} with vector notation; yields Eq.~ref{eq:#2}. 

1

linear algebra 
select imaginary parts 
1 
1 
0 
Select imaginary parts of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

0

complex values 
select real parts 
1 
1 
0 
Select real parts of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

complex values 
separate three vector components 
1 
3 
0 
Separate three vector components in Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2} and Eq.~ref{eq:#3} and Eq.~ref{eq:#4}. 

0


separate two vector components 
1 
2 
0 
Separate two vector components in Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2} and Eq.~ref{eq:#3} 

1


separate vector into two trigonometric ratios 
1 
2 
1 
Separate vector in Eq.~ref{eq:#2} into components related by angle $#1$; yields Eq.~ref{eq:#3} and Eq.~ref{eq:#4}. 

1


simplify 
1 
1 
0 
Simplify Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

66


solve for X 
1 
1 
1 
Solve Eq.~ref{eq:#2} for $#1$; yields Eq.~ref{eq:#3}. 

0


square root both sides 
1 
2 
0 
Take the square root of both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2} and Eq.~ref{eq:#3}. 

6


substitute LHS of expr 1 into expr 2 
2 
1 
0 
Substitute LHS of Eq.~ref{eq:#1} into Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

70


substitute LHS of five expressions into expr 
6 
1 
0 
Substitute LHS of Eq.~ref{eq:#1} and LHS of Eq.~ref{eq:#2} and LHS of Eq.~ref{eq:#3} and LHS of Eq.~ref{eq:#4} and LHS of Eq.~ref{eq:#5} into Eq.~ref{eq:#6}; yields Eq.~ref{eq:#7}. 

0


substitute LHS of four expressions into expr 
5 
1 
0 
Substitute LHS of Eq.~ref{eq:#1} and LHS of Eq.~ref{eq:#2} and LHS of Eq.~ref{eq:#3} and LHS of Eq.~ref{eq:#4} into Eq.~ref{eq:#5}; yields Eq.~ref{eq:#6}. 

2


substitute LHS of six expressions into expr 
7 
1 
0 
Substitute LHS of Eq.~ref{eq:#1} and LHS of Eq.~ref{eq:#2} and LHS of Eq.~ref{eq:#3} and LHS of Eq.~ref{eq:#4} and LHS of Eq.~ref{eq:#5} and LHS of Eq.~ref{eq:#6} into Eq.~ref{eq:#7}; yields Eq.~ref{eq:#8}. 

0


substitute LHS of three expressions into expr 
4 
1 
0 
Substitute LHS of Eq.~ref{eq:#1} and LHS of Eq.~ref{eq:#2} and LHS of Eq.~ref{eq:#3} into Eq.~ref{eq:#4}; yields Eq.~ref{eq:#5}. 

2


substitute LHS of two expressions into expr 
3 
1 
0 
Substitute LHS of Eq.~ref{eq:#1} and LHS of Eq.~ref{eq:#2} into Eq.~ref{eq:#3}; yields Eq.~ref{eq:#4}. 

6


substitute RHS of expr 1 into expr 2 
2 
1 
0 
Substitute RHS of Eq.~ref{eq:#1} into Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

39


subtract X from both sides 
1 
1 
1 
Subtract $#1$ from both sides of Eq.~ref{eq:#2}; yields Eq.~ref{eq:#3}. 

16


subtract expr 1 from expr 2 
2 
1 
0 
Subtract Eq.~ref{eq:#1} from Eq.~ref{eq:#2}; yields Eq.~ref{eq:#2}. 

4


sum exponents 
1 
1 
0 
Sum exponents on LHS and RHS of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

0


sum exponents LHS 
1 
1 
0 
Sum exponents on LHS of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

0


sum exponents RHS 
1 
1 
0 
Sum exponents on RHS of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

0


swap LHS with RHS 
1 
1 
0 
Swap LHS of Eq.~ref{eq:#1} with RHS; yields Eq.~ref{eq:#2}. 

14


take curl of both sides 
1 
1 
0 
Apply curl to both sides of Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 

1

linear algebra 